3 ms·
Yes, 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 impl
by more_original 12y ago
Yes, 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