> 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

Reply via email to