[Haskell-cafe] Verifying Haskell programs vs. generating verified Haskell programs
alex.solla at gmail.com
Tue Jun 21 19:48:17 CEST 2011
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 . 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...
More information about the Haskell-Cafe