On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger <squar...@gmail.com> wrote:
> 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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
