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

[Alexander Solla]

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?)
>

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110621/34a36f55/attachment.htm>