Re: Compiler Correctness

our moderator writes:
>[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...


Also relevant -- although not quite the same thing -- is George Necula's
work on "certifying compilers" (e.g. his PLDI98 paper). Here the idea is
not to prove the compiler correct, but to prove its *output* correct, in
at least limited respects.


The idea is that the compiler annotates the output code with a proof that
the code satisfies certain constraints. That proof is then checked by an
independent checker -- *much* smaller and simpler than a theorem prover.
The result is that you can trust the compiler's output to have certain
properties even if you're not sure the compiler itself is correct. (He
also found it a very effective tool for compiler debugging.)
--
spsystems.net is temporarily off the air; | Henry Spencer
mail to henry at zoo.utoronto.ca instead. | henry@spsystems.net

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