On Mon, Sep 15, 2008 at 2:43 PM, Robin Green <[EMAIL PROTECTED]> wrote: > On Mon, 15 Sep 2008 13:05:11 -0300 > "Rafael C. de Almeida" <[EMAIL PROTECTED]> wrote: >> Someone mentioned coq, I read a bit about it, but it looked really >> foreign to me. The idea is to somehow prove somethings based only on >> the specification and, after that, you write your code, based on your >> proof? > > No. There are 3 main ways of using Coq: > > 1. Code extraction. You write your code in Coq itself, prove that it > meets your specification, and then use the Extraction commands to > convert the Coq code into Haskell (throwing away all the proof bits, > which aren't relevant at runtime). > > 2. Verification condition generation (VCGen) - you write your code in > some "ordinary" language, say Haskell, and annotate it with > specifications. Then you run a VCGen tool over it and it tries to prove > the trivial things, and spits out the rest as "verification conditions" > in the language of Coq, ready to be proved in Coq.
That seemed to me the most interesting way of using it. After all, I already like writing my programs in Haskell, not sure if I'd like Coq better for programming. Also, that could work with code I've already written. Do you know of a VCGen tool that works well with Haskell and some other language such as Coq (doesn't need to be coq)? A quick search on google didn't give me much. > 3. A combination of both of the above approaches - you write your code > in Coq, ignoring the proof at first, and then verification conditions > (called "obligations" in Coq) are generated. This is experimental. The > commands that begin with "Program" in Coq are used for this. > > None of these involve writing the same code twice in different > languages. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
