The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

> I've always thought that it would be a more interesting contest
> if the problems that were posed weren't so focused on imperative
> issues in programming (e.g., sort an array using updates).  A
> more functional-oriented contest would play to the strengths
> of not only Coq, but I suspect Isabelle, ACL2, PVS, etc. and
> let us do something deeper.

As two of the organizers, we'd like to comment on this.

Our problems were not so focused on imperative programming. As stated in 
the competition description, participants were free to prove purely 
applicative implementations of the proposed algorithms. And indeed, 
among the medalists, one gold medal was awarded to a ACL2 solution and 
one silver medal to a PVS solution. Both were obviously purely 
applicative. We also received several Coq and Isabelle solutions.

We deliberately chose an imperative style to describe the problems only 
to make the competition more accessible to a larger set of participants.

--
Jean-Christophe and Andrei