The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

Dear Stéphane,

Good points.
The Ynot library claims to support IO for Coq:
http://ynot.cs.harvard.edu/
but this may not be suitable for the shootout.

My question was a bit provocative,
but I would be interested in any kind of fair benchmarks for say Coq
vs OCaml vs haskell.

Best,

Bas

On Tue, Mar 2, 2010 at 10:56 AM, Stéphane Glondu 
<steph AT glondu.net>
 wrote:
> Bas Spitters a écrit :
>> Did anyone ever try to line-up Coq in the programming language shoot-out?
>> http://shootout.alioth.debian.org/
>
> Not that I know of.
>
> The interface with these benchmarks is done with IOs, which Coq doesn't
> have. If you want to perform IOs from Coq code, I think you'll have to
> extract it first... at least, this is the most natural way IMHO. But
> then, you'll be benchmarking the target language (which could be OCaml,
> Haskell or Scheme), not really Coq itself. I guess for most of programs
> in one of the possible target languages (in the purely functional
> fragment, in the proposed benchmarks anyway), one can manage to write
> something in Coq that extracts to it... proving properties about them is
> another thing.
>
> Another approach would be to wrap IOs in some kind of script, that would
> parse the input, generate apropriate Coq input file, run it through
> coqtop, then parse the output and turn it into the expected format. It
> might be funny to compare Coq to other programming languages this way.
> But this would also benchmark the pre/post-processing steps (for which
> another language has to be chosen, too).
>
>
> Best regards,
>
> --
> Stéphane
>