The Coq mailing list

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

FWIW, This paper -- describing a case study using extraction to produce a drop-in replacement for a Haskell window manager -- which I found based on a few of the comments I got in response to my query, provides a pretty nice overview of the issues that arise when trying to integrate extracted code into a legacy environment.

http://www.staff.science.uu.nl/~swier004/Publications/XmonadInCoq.pdf

Slides: http://www.staff.science.uu.nl/~swier004/Talks/BrouwerExtraction.pdf

My favorite qotation: If you want to do formal verification, sed should not be a mandatory part of your toolchain.

Kevin

On Thu, Mar 6, 2014 at 7:38 AM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

:-) I appreciate the response (really). I'll go do that. --Kevin

On Thu, Mar 6, 2014 at 7:23 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

My response here is in danger of coming across as rudely close to "RTFM," but: have you read the whole chapter of the Coq reference manual called "Extraction of programs in Objective Caml and Haskell"?  There I think you find all the commands you need to do extraction to alternative type representations, as long as your original code contains no explicit pattern matches on those types.

On 03/06/2014 07:14 AM, Kevin Sullivan wrote:

Thanks Greg and Cedric,

I'm not necessarily committed to Haskell. What hooks did you, Greg, have in mind for doing such mappings/replacements when extracting to OCaml?

Kevin

On Wed, Mar 5, 2014 at 11:05 PM, Greg Morrisett <greg AT eecs.harvard.edu> wrote:

I don't have experience extracting Haskell, but when I do OCaml,
I tend to map certain things (ascii, nat) to native OCaml
types (e.g., char, bignum).  I agree it's less than optimal, but
that's the price of interoperability with legacy code...

Anyway, there are good hooks for doing this kind of replacement.