The Coq mailing list

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

Very interesting.
I guess you are referring to your paper:
http://www.lix.polytechnique.fr/~mboes/papers/padl10.pdf

Could you explain more about the status of your implementation for Coq?

I would be keen to try it on our real number computations:
Certified Exact Transcendental Real Number Computation in Coq (Russell 
O'Connor)
http://arxiv.org/abs/0805.2438
A computer verified, monadic, functional implementation of the
integral (Russell O'Connor, Bas Spitters)
http://arxiv.org/abs/0809.1552

In the latter paper we experimented with threaded execution of the
extracted program.
We did this manually, but easily,  for OCaml, giving a 3 times speed
up on a four processor machine.
We  tried to do it semi-automatically in haskell.
I.e. we defined
par  :: a -> b -> b
pseq :: a -> b -> b
by trivial projections in Coq and then a small modification of the
extracted code would do.
Unfortunately, Coq's modules do not extract to haskell.

Finally, I understand that Isabelle allows threaded execution.
# ML: support for Poly/ML 5.3.0, with improved reporting of compiler
errors and run-time exceptions, including detailed source positions.
# Parallel checking of nested Isar proofs, with improved scalability
up to 8 cores.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/

Would your approach allow something similar?

Best,

Bas

On Tue, Mar 2, 2010 at 10:13 PM, Mathieu Boespflug 
<mboes AT tweag.net>
 wrote:
> Hi,
>
>> There is anecdotal evidence that Coq looses a factor between 5-50 in
>> speed to the extracted OCaml program.
>> It would be nice if we could substantiate this.
>
> In my experience, if using the Coq VM (vm_compute tactic), performance
> loss compared to state of the art compilers for functional languages
> is limited to a factor of 5-10, which is a typical performance gap
> between bytecode interpreters and compilation to native code. There is
> current work nearing completion, however, on adding a new execution
> mechanism to Coq where Coq terms are compiled to native code. This
> execution mechanism uses the stock OCaml compiler as a backend to
> generate native code so execution should be about as fast as any
> regular OCaml program.
>
> -- Mathieu
>