On Tue, Jun 21, 2011 at 3:31 AM, 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?)
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.