Re: Compiler Correctness

torbenm@app-1.diku.dk (=?iso-8859-1?q?Torben_=C6gidius_Mogensen?=)
11 Feb 2006 13:15:35 -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)
[8 later articles]
| List of all articles for this month |

From: torbenm@app-1.diku.dk (=?iso-8859-1?q?Torben_=C6gidius_Mogensen?=)
Newsgroups: comp.compilers
Date: 11 Feb 2006 13:15:35 -0500
Organization: Department of Computer Science, University of Copenhagen
References: 06-02-053 06-02-061
Keywords: theory, debug

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



Post a followup to this message

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