Re: Compiler Correctness

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


Andrew Appel, has been doing related work in this area. He also gives a
talk where he explains point by point why Perlis was off the mark.
Unfortunately, I can't find a pointer to it now. The FPCC project tries
to establish the type-safety of SPARC machine code from a minimal TCB.
Some interesting facts that come from the FPCC project are.


A minimal proof verifier is 1-2 thousand lines of C code. This proof
verifier uses no library calls. It's designed so you can compile it to
assembly and can eyeball the output of the compiler. The basic logic
has around 10 axioms from which all of modern mathematics can be
derived. Then there is a 4000 line partial specification of the SPARC
machine semantics.


Proofs of compiler correctness are more involved. However, a minimal
proof verifier I suspect would be on order of Appel's verifier. The
statement of the theorem needs to include the machine semantics so
let's say another 4000 lines specification, plus the semantics for the
C subset. I'll guess this also is on the order of 2000 lines.


I'd say there is under 10 thousands lines of stuff you have to eye ball
very carefully, before you trust the result and believe the proof is true.


One problem with the POPL06 result is that their correctness result only
applies to program that are known to terminate. This is a flaw in the
way their semantics is set up.


In any case. It's been demonstrated that simple proof verifiers can be
written in about 2000 lines of C. To trust any machine checked proof is
simply a matter of encoding a known sound logic, encoding the statement
of your theorem in that logic and then generating the proof to be checked.


For compiler correctness the statement of the theorem is relatively
complex. You need a semantics for the source and target languages. A
good deal of the challenge in a compiler correctness proof is the
statement of the theorem.


Dan (former student of Andrew W. Appel)

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