The Coq mailing list

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

Dear Colleagues:

A grad student of mine is looking at integrating Haskell code extracted from a Coq specification into an industrial environment. The environment in this case includes a standard Haskell installation, the yesod web service framework, etc. The Coq spec uses types such as Coq String, Coq Z, etc. When we extract code, we end up with extracted versions of Coq string, Coq Z etc. But the frameworks expect the use of their "built-in" analogs, e.g., Haskell's String type. 

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? Or for swapping out definitions extracted from Coq and allowing references to be bound to the native versions? Clearly doing such a substitution increases the TCB, nor is it necessarily safe, in that the semantics might not always match exactly.

So, again, what is the best practice in this regard?

Thanks,

Kevin