Re: [Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

On Mon, Sep 15, 2008 at 2:43 PM, Robin Green wrote:

On Mon, 15 Sep 2008 13:05:11 -0300 "Rafael C. de Almeida" 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.