The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Xavier, Thanks very much for this information. It's *very* helpful. 

On Thu, Mar 6, 2014 at 1:03 PM, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

On 06/03/14 01:49, Kevin Sullivan wrote:
> The question is, what's the current best practice for "bridging" from Coq's
> types to analogs provided and used natively in target languages and related
> frameworks?

For what it's worth, here is what I do for CompCert, using extraction
to OCaml.

1- Before extraction, use

Require Import ExtrOcamlBasic.
Require Import ExtrOcamlString.

This maps Coq's booleans, lists, pairs, and characters to OCaml's.
Already a good start.

2- For (exact) integers and strings, I prefer to keep Coq's definitions
unchanged and convert to/from OCaml's integers and strings as needed.
You can find the conversion functions I use in the lib/Camlcoq.ml file
of the CompCert distribution (http://compcert.inria.fr/).

3- The more I write OCaml code that must interface with Coq-extracted
code, the more I tend to use Coq's datatypes in the OCaml code.  For
example, Coq's "Z" type is a half-decent implementation of big
integers: not as fast as OCaml's bignums (or alternatives like
Zarith), but not prohibitively slow either, and provably correct!

Hope this helps,

- Xavier Leroy