[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.