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
