[147261] in cryptography@c2.net mail archive
Re: [Cryptography] The Case for Formal Verification
daemon@ATHENA.MIT.EDU (Tim Newsham)
Sun Sep 22 13:40:26 2013
X-Original-To: cryptography@metzdowd.com
In-Reply-To: <loom.20130919T123047-51@post.gmane.org>
Date: Thu, 19 Sep 2013 22:42:59 -1000
From: Tim Newsham <tim.newsham@gmail.com>
To: Derek Jones <derek@knosof.co.uk>
Cc: "cryptography@metzdowd.com" <cryptography@metzdowd.com>
Errors-To: cryptography-bounces+crypto.discuss=bloom-picayune.mit.edu@metzdowd.com
> 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/
With all due respect, most of the points you make are ridiculous.
For example, you point out that the certified C compiler will not
make any guarantees about code that relies on undefined behavior.
Well, of course! Being certified doesn't magically fix your specification!
Certified just says the implementation matches the specification!
And to suggest that such a project is misguided because it places
blind trust in coq (and because it is written in ocaml?!) shows a
misunderstanding of the proof tools. There is a very small core of
trust that you need to have faith in and it is backed by solid theory
and is a much more solid foundation for building on than just about
any other software we have in computer science. I don't see how in
any way you can compare the f2c translator to this effort.
--
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
_______________________________________________
The cryptography mailing list
cryptography@metzdowd.com
http://www.metzdowd.com/mailman/listinfo/cryptography
