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

2011/6/21 Jason Dagit

...

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

On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger wrote: 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