The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

I'm not aware of any API for that, but for what its worth, there is one recent work that aims at extracting Ruby [1].

So if not better pops up, I guess you could check the rep for some guidelines :)

Anyway, good luck with that!

[1] https://github.com/mzp/coq-ruby/commits/master

2012/3/1 <yannick_duchene AT yahoo.fr>

Hi all,

If people don't mind about a beginner question, I have one: one can extract an
Ocaml program from a proved specification. Are there some ways to extract an
SML program and/or an Ada program?

If not, if there a kind of semantic API or anything else to help with this? And
is such an attempt, dangerous, useless, difficult?

I searched the web, but failed to locate relevant materials for that matter.

With thanks.

Yannick D.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.