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

On Wed, Jun 22, 2011 at 8:11 AM, Dominic Mulligan < dominic.p.mulligan@googlemail.com> wrote:

...

There's a second (haha) approach, which I use basically every day.

...

Use the typing language fragment from a strongly typed programming language to express a specification, and then rely on "free" functions/theorems and the Howard-Curry isomorphism theorem to guarantee correctness of implementation relative to the specification.

How does this count as a distinct approach to the problem? It's essentially what happens when you verify a program in Coq.

Further, there's much too sharp a distinction in the OP's mind between constructing a verified program in a proof assistant and verifying an existing program.

Yes, I agree about your further point. And if we agree there is little-to-no distinction between using an external tool and an internal sub-language, my point becomes even weaker. But I do think we can agree there is some difference between a total language (i.e., a proof assistant) versus a partial language with strong typing (like Haskell) versus a memory-poking-and-peeking magma (like C). My point was that we don't necessarily have to go for a total language to get logical proof. We can instead rely on derivable/free functions for most of the verification, and paper-and-pencil proof/proof by inspection/etc. for the rest.