> The CompCert people are claiming a formally verified compiler and I > think this claim is very misleading to say the least.
I don't find it misleading at all and I think perhaps the confusion is your notion of what formally verified means. >> 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 > > 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) What I am saying is that you do not need to trust the coq code. There is actually very little of the coq tool that you do need to trust. That is the part of coq that performs type checking. The type checker is what verifies proofs. It is a small part of coq and most of coq is not trusted and generates terms that still must pass the type checker. Neither do you need to put a lot of faith in the ocaml compiler, the cpu or spend a lot of time worrying about cosmic rays flipping the bits during computation. Yes, some flaw could potentially lead to an incorrect computation on a certain cpu or a certain memory bit in a certain machine during a certain computation. But the coq type checker has been compiled on many machines and with many versions of the ocaml library and the odds of a random error behaving in a way that just happens to validate an invalid proof term more miniscule (as in, I would be more worried about your spontaneously tunneling into my livingroom due to quantum effects to resume the rest of this conversation). There is a small part of coq that you DO have to trust. If this part is incorrect it could invalidate all of the proofs. However, this part of coq is backed by strong theory and has had many eyes on it. And while it is possible that an error here could lead to a bad proof, it is by no means assured. > Derek M. Jones tel: +44 (0) 1252 520 667 -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com _______________________________________________ The cryptography mailing list cryptography@metzdowd.com http://www.metzdowd.com/mailman/listinfo/cryptography