Credible Compilation

Current compilers provide no evidence that they are operating correctly - you give them your program, and they give you a bunch of bits back in the form of an executable. You have to take it on faith that the compiler compiled your program correctly.

The goal of the credible compiler project is to develop a compiler that gives you, in addition to the executable, a proof that the executable correctly implements your program. We believe that this approach will help developers find and eliminate bugs in compiler passes, allow large groups of mutually untrusting people to collaborate productively on the same compiler, make it possible to aggressively upgrade large, stable compilers without fear of inadvertantly introducing undetected errors, and promote the use of compilers that are customized for specific application domains.

We are initially focusing on proving the correctness of individual compiler transformations such as constant folding, induction variable elimination, loop unrolling, etc.