On 5/25/23 10:06, Guy Sotomayor via cctalk wrote:
The way SPARK works is that you have code and then can
also provide
proofs for the code. Proofs are you might expect are *hard* to write
and in many cases are *huge* relative to the actual code (at least if
you want a platinum level proof).
...and we still get gems like the Boeing 737MAX...
--Chuck