Re: Compiler Correctness

Neelakantan Krishnaswami wrote:
>> I have a simple question. Can we prove that a compiler is correct? I
>> mean we are given a language with it's syntax and semantics and a
>> compiler whose correctness needs to be proved. Is this theoretically
>> possible?
>
> Yes, it is. In the POPL 2006 conference proceedings, Xavier Leroy
> reported on his efforts implementing a provably-correct compiler for a
> subset of C.
>
> The proof is extremely large, however, and in order to ensure the
> proof's correctness he had to develop the compiler in a theorem
> proving system that verified the correctness of all his proofs.
>
> "Formal certification of a compiler back-end, or: programming a
> compiler with a proof assistant"
>
> <http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf>
>
> [Interesting paper. I wonder how likely it is that the tools, which
> are not small, or the set of axioms have bugs that could affect the
> validity of the proof. If it sounds like I'm channelling the famous
> 1979 proof paper by Perlis et al, it's not surprising since he was my
> thesis advisor. -John]


A lot of the design of these tools has been shaped in specific
response to Perlis's paper.


Basically, the idea is that a theorem prover is inherently
untrustworthy. It's large, complex, and relies on very advanced math
for its correct operation -- it will have bugs with basically 100%
certainty.


So what these programs do is construct the actual proof of the theorem
as a data structure which you can print out. Then, you can write a
proof *checker* to verify the operations that the theorem prover has
carried out.


A proof checker is much smaller than the theorem prover; usually they
are a few hundred lines of code. Thus, they are small enough that
Perlis's criticisms don't apply to them -- the checkers are programs
that people can manually verify and easily write multiple competing
implementations to increase trust.


So, the process is:


1. You develop your proof interactively with the prover.
2. You dump out the proof and run your proof checkers on it.
3. If it says your proof is good, then you're done.
4. If it says your proof is bad, then you curse, and fix the
      bug in the theorem prover and redo your proof.


Interestingly, this is a technique that Leroy used in his compiler.
For example, the register allocator would find a coloring, and then
he'd run a checker on it to ensure that it was okay before proceeding.
If the check failed, then his compiler would report that it failed to
compile that program rather than emitting incorrect code.


IIRC, the logic in Coq is equivalent to ZFC with countably many
inaccessible cardinals. That's a very rich foundation, but still
pretty conventional.


--
Neel Krishnaswami
neelk@cs.cmu.edu

Return to the comp.compilers page.
Search the comp.compilers archives again.