Hello Haskell fellows,
<br>
<br>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).
<br>
<br>(0) Programming in any language and then verifying it with an external 
theorem prover
<br>(1) Specifying the program in a proof language and then generating 
program code out of it (like in the CompCert project)
<br>
<br>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?)
<br>
<br>Best regards,
<br>Uli Kastlunger
<br>
<br>[0] <a class="moz-txt-link-freetext" href="http://compcert.inria.fr/">http://compcert.inria.fr/</a>