3 ms·
People certainly have written real software using formal methods: http://compcert.inria.fr/ http://compcert.inria.fr/ is a good example. Of course this does no
by gsg 15y ago
People certainly have written real software using formal methods: http://compcert.inria.fr/ http://compcert.inria.fr/ is a good example.
Of course this does not constitute an argument that programming must be taught as a formal discipline, but it does indicate that formal methods can be useful in some circumstances.
- microtherion 15y agoThanks, interesting example! Interestingly, http://compcert.inria.fr/release/Changelog http://compcert.inria.fr/release/Changelog mentions various "bug fixes" in almost every release, and the mentions of "successful tests" are not quite canonical either, but it certainly looks like a successful, nontrivial program.
- gsg 15y agoYes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts). It does make a nice poster child for formal methods though.