Submitting this for historical interest and in case there’s lessons to learn. The Larch system and approach was basically the predecessor of things such as Frama-C for C apps or SPARK for Ada apps. As soon as they made it, a bunch of interface projects sprung up to apply it to C, Ada, Smalltalk, and Modula-3. I’m not sure about most of those but Modula-3 did get parts of its standard library verified via Larch. So, a memory-safe alternative to C++ with a partly-verified stdlib in the 90’s. Work on these approaches, esp through Praxis’s SPARK project, kept increasing the automation to knock out more and more types of errors with [hopefully] less and less effort on part of programmers.
Today, programmers without formal methods experience can pick up a book [1], practice a bit, and build something as useful as a DNS server [2] free from common vulnerabilities.
Submitting this for historical interest and in case there’s lessons to learn. The Larch system and approach was basically the predecessor of things such as Frama-C for C apps or SPARK for Ada apps. As soon as they made it, a bunch of interface projects sprung up to apply it to C, Ada, Smalltalk, and Modula-3. I’m not sure about most of those but Modula-3 did get parts of its standard library verified via Larch. So, a memory-safe alternative to C++ with a partly-verified stdlib in the 90’s. Work on these approaches, esp through Praxis’s SPARK project, kept increasing the automation to knock out more and more types of errors with [hopefully] less and less effort on part of programmers.
Today, programmers without formal methods experience can pick up a book [1], practice a bit, and build something as useful as a DNS server [2] free from common vulnerabilities.
https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736
http://ironsides.martincarlisle.com/