The Coq mailing list

[Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>]

On 2012/03/01, at 14:48, 
yannick_duchene AT yahoo.fr
 wrote:

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

I'm not aware of any off-the-shelf extraction for either SML or Ada.
There is already support for Haskell and Scheme in addition to OCaml,
and external backends for ruby (already mentioned) and Scala [1].

[1] https://bitbucket.org/yoshihiro503/coq2scala/src

If there is a strong need, I suppose that exporting to SML should not be too
difficult, as extract OCaml code is essentially Core ML + modules, so this is 
just about
changing the syntax.
Extraction to Ada seems another problem: how do you encode the lambda-calculus
in Ada?

Jacques Garrigue