Tim, > With all due respect, most of the points you make are ridiculous.
Could you please explain why you think they 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! Where did the word "certified" come from? I have not said anything about magically fixing a specification. The CompCert people are claiming a formally verified compiler and I think this claim is very misleading to say the least. > 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 I did not say that this project was misguided. > 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 Yes, the axioms. These need to be small in number and 'obviously' correct; something that cannot be said of the source code of coq. The nearest I can think of is the Lisp subset written in itself in under a 100 lines (my memory is vague on this point) > 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. Why not? What work has been done on the coq+other tools that has not been done on f2c? I describe work that was done to try and show the correctness of a Model Implementation for C here: http://shape-of-code.coding-guidelines.com/2011/05/02/estimating-the-quality-of-a-compiler-implemented-in-mathematics/ [ My original post to this list bounced, so I am reposting it here now), it cam ebefore the message it is replying to] _______________________________________________ The cryptography mailing list cryptography@metzdowd.com http://www.metzdowd.com/mailman/listinfo/cryptography