[Cryptography] The Case for Formal Verification

Tim Newsham tim.newsham at gmail.com
Fri Sep 20 04:42:59 EDT 2013


> 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


More information about the cryptography mailing list