CompCert - Compilers you can formally trust

Also worth reading: the paper that found bugs in the proven-correct compiler: <a href="http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf" rel="nofollow">http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf</a><p>(okay, so only a portion of the compiler is proven correct, and they didn't find any bugs in that portion).<p>Note also that a compiler with a proof isn't necessarily correct - it just means that you've pushed all your bugs into your description of the rules of C and of the target architecture. Since neither C nor any common CPU architecture have a formal semantics, someone has to read the (english) description and convert it to a description in their theorem proving software, and there's no reason to believe this will be easy.

This old Knuth quote seems apt:<p><i>"Beware of bugs in the above code; I have only proved it correct, not tried it."</i>

I'm confused. The title made me think "list of compilers I can trust", but the website provides no such thing. It looks to me like they've written their own compiler.

To be realistic: The frontend is not verified. Only very few optimizations are done. It only seems to have a PPC backend.<p>However, i still think verified compilers are the future. It will just take two or three decades until we see them at LLVM quality.

I seem to remember a CPU that was stack-based that was built for correctness. I think it was called the Viper, but I cannot seem to find it. It would be logical to me to run your formally trusted compiler on a chip designed the same way.

Would someone explain "formally trust" in this sense?