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

[Rafael Almeida]

On Mon, Sep 15, 2008 at 2:43 PM, Robin Green <greenrd at greenrd.org> wrote:
> On Mon, 15 Sep 2008 13:05:11 -0300
> "Rafael C. de Almeida" <almeidaraf at gmail.com> 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.