[SystemSafety] Safety and programming languages

[Stefano Costa]

Thanks a lot Rod for your insights.

We're aware of MISRA and use the rules a lot, with a highly effective 
static analysis tool in place for this (Eclair by Bugseng). More often, 
the coding style and coding rules are a mix of MISRA, company specific 
(our clients) and derived from other manuals.

I agree on using MISRA and other effective language enforcing rules 
since the beginning of a development when C (and C++) is a must. 
Toolchains themselves (starting with plain old GCC) if correctly set 
with all features taken into account are good at spotting weaknesses.

I'm looking forward at using ADA and Rust in real development, while up 
to now we only did PoC and Academic stuff. Ferrocene is a very serious 
initiative and I'm pondering about joining.

S

On 16/03/22 10:13, Roderick Chapman wrote:
> 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
> 
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

-- 
Stefano Costa
M +39 335 6565749
http://www.bluewind.it