[Haskell-cafe] Verifying Haskell programs vs. generating verified Haskell programs

[Uli Kastlunger]

2011/6/21 Jason Dagit <dagitj at gmail.com>

> On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger <squark42 at gmail.com>
> wrote:
> > Hello Haskell fellows,
> >
> > recently there has been a huge progress in generating real programs by
> > specifying them in interactive theorems prover like Isabelle or Coq, in
> > particular a verified C Compiler has been generated out of a
> specification
> > in Coq [0]. Furthermore it is often stated, that it is easier to reason
> > about functional languages. So in my opinion there are two approaches
> > building verified software (e.g. in case of compilers: verify that the
> > semantics of a high-level language maps correctly to the semantics of a
> > low-level language).
> >
> > (0) Programming in any language and then verifying it with an external
> > theorem prover
> > (1) Specifying the program in a proof language and then generating
> program
> > code out of it (like in the CompCert project)
> >
> > I think both ideas have their (dis)advantages. The question is, which
> > concept will be used more frequently? In particular how hard would it be
> to
> > build something like CompCert the other way around (in this case writing
> a C
> > compiler in SML and proving its correctness?)
>
> Proving the correctness of a C compiler is quite a challenge
> regardless of how you write the compiler.  The reason there is that
> you need a well-defined version of C so that you have a spec for the C
> compiler that can be used in formal methods approaches.
>
> Assuming you've done that, then it seems like SML would lend itself
> just fine to being your implementation language.  Tools like
> Isabelle/HOL could be used as your external theorem prover.
>
> If your compiler is fully verified then that's great news but you
> could still write buggy programs with it.  Likewise, you could have a
> proven your program is correct with respect to the formal semantics of
> the language and your program specification but then used a buggy
> compiler.  So it seems to me that not only do the two approaches you
> outline have different advantages but they are solving different and
> closely related problems.
>
> I'm no expert with compcert, but as I understand it their approach is
> to only do semantic preserving changes to the program at each step in
> the translation from C source to binary.  I'm not sure what they used
> as their specification of C and it seems like the correctness of their
> approach would still depend on a spec.
>
> I hope that helps,
> Jason
>

First, a small correction to CompCert: I got this wrong, it generates Caml
Code not SML Code.

You are right, to do a verified Compiler, you need a specified Version of C
and also a specified Version of you target assembly language. But the
question is, if it is then more applicable to write your Compiler in a
language like Haskell and then verify it, or if you do it the other way
around, use a specification language which can generate verified code.

br,
uli
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110622/bd65120e/attachment.htm>