Re: Compiler Correctness

> 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>
--
Neel Krishnaswami
neelk@cs.cmu.edu
[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]

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