Comment by nequo

My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics.

So CompCert seems to me to aim to help mission-critical software to move away from C, and possibly into Coq/Isabelle/etc., except for the purposes of compilation to machine code.