<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I guess I might as well jump in...</p>
<p>For SPARK, start with our "greatest hits" compilation here:</p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">R. Chapman and F. Schanda, “Are we there yet? 20 years of
industrial theorem proving with SPARK.”<span
class="Apple-converted-space"> </span></span><em
style="margin: 0px; padding: 0px; border: 0px; font-size: 14px;
vertical-align: baseline; caret-color: rgb(51, 51, 51); color:
rgb(51, 51, 51); font-family: Helmet, Freesans, sans-serif;
font-variant-caps: normal; font-weight: 400; letter-spacing:
normal; orphans: auto; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: auto;
word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; text-decoration: none;">Invited
Keynote Paper</em><span style="caret-color: rgb(51, 51, 51);
color: rgb(51, 51, 51); font-family: Helmet, Freesans,
sans-serif; font-size: 14px; font-style: normal;
font-variant-caps: normal; font-weight: 400; letter-spacing:
normal; orphans: auto; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: auto;
word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">, Proceedings of Interactive Theorem Proving (ITP) 2014.
Springer-Verlag LNCS Vol. 8558, pp. 17-26.</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">I can supply PDF of that.<br>
</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">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.</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">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.<br>
</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">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).</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;">That's it for now...</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;"> - Rod</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;"><br>
</span></p>
<p><span style="caret-color: rgb(51, 51, 51); color: rgb(51, 51,
51); font-family: Helmet, Freesans, sans-serif; font-size: 14px;
font-style: normal; font-variant-caps: normal; font-weight: 400;
letter-spacing: normal; orphans: auto; text-align: start;
text-indent: 0px; text-transform: none; white-space: normal;
widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto;
-webkit-text-stroke-width: 0px; background-color: rgb(255, 255,
255); text-decoration: none; display: inline !important; float:
none;"><br>
</span></p>
</body>
</html>