> 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
