<br><br><div class="gmail_quote">On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger <span dir="ltr"><<a href="mailto:squark42@gmail.com">squark42@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
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></blockquote><div><br></div><div>There's a second (haha) approach, which I use basically every day.</div><div><br></div><div>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.</div>
</div><br>