Perry E. Metzger <perry <at> piermont.com> writes: > CompCert is a fine counterexample, a formally verified C compiler: > http://compcert.inria.fr/ > It works by having a formal spec for C, and a formal spec for the > machine language output. The theorem they prove is that the
The claim of CompCert being a formally verified C compiler is wildly overstated: http://shape-of-code.coding-guidelines.com/2013/03/10/verified-compilers-and-soap-powder-advertising/ It is a good start, but they still have lots of work to do. _______________________________________________ The cryptography mailing list cryptography@metzdowd.com http://www.metzdowd.com/mailman/listinfo/cryptography
