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