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

[Uli Kastlunger]

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

Best regards,
Uli Kastlunger

[0] http://compcert.inria.fr/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110621/2ae022eb/attachment.htm>