The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi coq-club,

Lately, I had the opportunity to attend a very interesting talk about
Dafny [1], which highlighted the recent VSTTE competition (talk about
the  results at [2]). From the results, it seem that 7 teams made a
submission that was using Coq. Unfortunately, I cannot find any using
a search engine. So, I am turning to the coq-club list, hoping that
some of these people would agree to make their submissions public, and
discuss them.

Now, on an higher level: looking at the variety of entries in the
competition, and the set of problems, I think that the VSTTE
competition is a good example of stuff that could foster some "cross
community" interaction (say, "this is how people formalise this very
same problem in Foo, and Bar"), and as such, the Coq community may
gain something of having public and well-crafted solutions [3].

But, it could as well create some discussion among Coq users ("these
are two different ways of formalising the same thing in Coq, what are
the relative merits of both solutions ?"). Note that this is not
limited to this particular context of program verification, and that
[4] may also be relevant. And [5]. And I am sure that there are many
interesting sets of problems that have been used or could be used in
different verification systems/proof assistants/formalisation styles
to compare them.

Of course, wrapping up this e-mail w.r.t. its first paragraph, it may
be the case that Coq is not (yet) fit to solve the VSTTE kind of
problems (at least, in a reasonable, not too hairy manner). In which
case, making this public would help future users to avoid pitfalls.

With best regards
Thomas

[1] http://research.microsoft.com/en-us/projects/dafny/ or
http://rise4fun.com/Dafny/Fibonacci
[2] http://www.lri.fr/~filliatr/pub/slides-vstte-12.pdf
[3] I take as an axiom that it is indeed possible ;)
[4] http://www.cs.ru.nl/~freek/100/
[5] http://projecteuler.net/