[147235] in cryptography@c2.net mail archive
Re: [Cryptography] The Case for Formal Verification
daemon@ATHENA.MIT.EDU (Derek Jones)
Thu Sep 19 13:02:40 2013
X-Original-To: cryptography@metzdowd.com
To: cryptography@metzdowd.com
From: Derek Jones <derek@knosof.co.uk>
Date: Thu, 19 Sep 2013 10:33:09 +0000 (UTC)
X-Complaints-To: usenet@ger.gmane.org
Errors-To: cryptography-bounces+crypto.discuss=bloom-picayune.mit.edu@metzdowd.com
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
