Re: Compiler Correctness

henry@spsystems.net (Henry Spencer)
11 Feb 2006 13:15:56 -0500

          From comp.compilers

Related articles
Compiler Correctness Pramod.Patangay@gmail.com (pramod) (2006-02-07)
Re: Compiler Correctness find@my.address.elsewhere (Matthias Blume) (2006-02-07)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-11)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-11)
Re: Compiler Correctness torbenm@app-1.diku.dk (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Xavier.Leroy@inria.fr (Xavier Leroy) (2006-02-12)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
[7 later articles]
| List of all articles for this month |

From: henry@spsystems.net (Henry Spencer)
Newsgroups: comp.compilers
Date: 11 Feb 2006 13:15:56 -0500
Organization: SP Systems, Toronto, Canada
References: 06-02-053 06-02-061
Keywords: theory, debug

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



Post a followup to this message

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