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