[SystemSafety] Safety and programming languages

[Roderick Chapman]

I guess I might as well jump in...

For SPARK, start with our "greatest hits" compilation here:

R. Chapman and F. Schanda, “Are we there yet? 20 years of industrial 
theorem proving with SPARK.”/Invited Keynote Paper/, Proceedings of 
Interactive Theorem Proving (ITP) 2014. Springer-Verlag LNCS Vol. 8558, 
pp. 17-26.

I can supply PDF of that.

You should definitely know about MISRA. If you absolutely have to stick 
with C, then no excuse for not using MISRA, but be aware of its 
limitations. Look at how many of the rules are tagged "System" and 
"Undecideable" and make your own mind up if that's good enough for you.

As for Rust... it shows great promise. The "no_std" profile is 
interesting. There are research-level static verification tools. I have 
used MIRAI, Prusti, Kani and Crux-MIR and there are many more in the 
works. There are several problems: other than trait-bounds for generics, 
there is no standard contract language, so the different tools all try 
to define their own, so they're all different and lacking basic features 
such as quantifiers. None of these tools are commercially supported. 
Rust also lacks user-defined scalar types and so-called "Liquid Types", 
which are absolutely essential in SPARK.

See also the "Ferrocene" project from Ferrous Systems - that shows great 
promise to stabilize things and bring some much-needed provenance to the 
Rust world (at least for embedded systems).

That's it for now...

  - Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20220316/310c4999/attachment-0001.html>