The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

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