[user2342]

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

Thats my understanding too. Code is written in high level systems generating C as output. C becomes rather an implementation detail in a hopefully, more or less completely verified tool chain.