The Coq mailing list

[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.