The definitions of the semantics of both the input language and the output language of CompCert are operational. If you want to prove functional properties of p

The definitions of the semantics of both the input language and the output language of CompCert are operational. If you want to prove functional properties of programs written in the input language with respect to CompCert's definition, you will probably have to define Hoare-Floyd-style axiomatic semantics and then prove that this definition is equivalent to the operational semantics definition. An informal version of this proof for a toy language already exists in good textbooks (for instance Winskel's The Formal Semantics of Programming Languages). It is just a matter of scaling up to C and scaling down to the formally verified level. I should also point out that there is an ongoing research project that takes the same approach, with “Abstract-interpretation-based static analysis” instead of “verification of functional properties”: http://verasco.imag.fr/wiki/Main_Page http://verasco.imag.fr/wiki/Main_Page