The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

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