3 ms·
The proof is written in Coq, an automatic proof checker. Of course, Coq itself could have bugs, but it has a small trusted kernel and it produces proof objects
by more_original 12y ago
The proof is written in Coq, an automatic proof checker.
Of course, Coq itself could have bugs, but it has a small trusted kernel and it produces proof objects that can be checked, so what you get is much, much more reliable than the typical published proof in mathematics.
- userbinator 12y agoI think the parent's question might not be asking about whether the proof is correct in the "do all the statements in it logically hold" sense, but more like "is the proof a proof of what a 'correct' compiler should do", i.e. does the translation follow the C standard on one side, and the target machine's ISA on the other? Starting with the wrong assumptions can lead to valid reasoning to the wrong conclusion, and AFAIK Coq only helps with the "valid reasoning". In other words, if you have the wrong idea of what a compiler is, you can write one and a proof that it is correct. Humans have to be involved at some point to tell the machine what their idea of a correct compiler is. (Even if the machine somehow knows, that would also be a result of humans teaching it at some point in the past.)
- more_original 12y agoYes, that's a valid point. The idea is to first give a high-level formalisation of the C language definition and then to prove that the compiler correctly implements this. In the case of CompCert, the specification is given by a big-step operational semantics. Of course it's possible to make mistakes in it, but it is still small enough to be read and understood by humans (much more so than a whole compiler). From Coq one gets the guarantee that the compiler correctly implementes this language definition. To get an idea what the specification looks like, you may look at Fig.3 in http://gallium.inria.fr/~xleroy/publi/cfront.pdf http://gallium.inria.fr/~xleroy/publi/cfront.pdf