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

[Jason Dagit]

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