On Thu, 25 May 2023, Chuck Guzis via cctalk wrote:
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...
That wasn't a software problem, that was a criminally cheap management
problem - they deleted the comparator for the AoA indexer to save money.
g.
--
Proud owner of F-15C 80-0007
http://www.f15sim.com - The only one of its kind.
http://www.diy-cockpits.org/coll - Go Collimated or Go Home.
Some people collect things for a hobby. Geeks collect hobbies.
ScarletDME - The red hot Data Management Environment
A Multi-Value database for the masses, not the classes.
http://scarlet.deltasoft.com - Get it _today_!
