[pascal_cuoq]

The OP's problem is with the support for the exotic targets and the more recent additions to the C standard (C99, soon C11). CompCert targets only x86 and PowerPC, and does not support all the features of C99, not to mention the GCC extensions that everyone has come to rely on. In fact, in terms of these criteria it is uniformly worse than GCC 2.7.2.1 (although it is better at having verified, bug-free semantics).

[pdw]

That was only his second complaint.

  "First, compilers are fragile. While one would like to expect a minimum
  level of correctness and trustworthiness from a modern compiler, we
  can't, regardless of the compiler we use."

CompCert (had it been truly open source) would have provided that trustworthiness. And it can be ported to new architectures with the confidence that these ports won't silently break by random other changes.

[mansr]

There are two fundamental problems with CompCert: 1) there is no formal, machine-readable specification of the C language, and 2) there is no formal, machine-readable specification of the target architectures. CompCert may be formally verified, but it's not necessarily a C compiler (even ignoring that it implements only a subset of C), nor does it necessarily compile for the advertised architecture.

[qznc]

Addressing number 1) https://code.google.com/p/c-semantics/

Not perfect, but pretty good.