Re: Compiler Correctness

Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:


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


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


Proof systems usually rely on a very small set of basic axioms and
rules that are small enough that it isn't difficult to ensure the
correctness of their implementation (nor their validty w.r.t. standard
logical systems). Everything else is built on top of this small set,
and verified w.r.t. this. Hence, there is not usually any doubt that
machine-verified proofs actually prove the statements that they claim
to prove. The main problem is whether the proven statements actually
say what they are meant to say.


For example, a proof of correctnes of a compiler relies on the
correctness of the formal semantics of the source language and target
machine. There is usually no way to formally validate these
semantics, as the machines and languages they describe are rarely
defined by formalised semantics. So there would be some effort in
(verbally) relating the formal semantics to the informal descriptions
of language and machine.


I have not read the above paper, so I don't know how these points are
addressed there.


                Torben

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