The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> 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

Sorry for the late answer. Let me just confirm what Jacques already said :
no extraction to SML yet, but having a basic extraction to this language
is probably a few hour work if somebody wants to try : it should mostly
amount to adapting the syntax file ocaml.ml to a new sml.ml. Modules
(more precisely functors) could be an issue, but the trick I use for
Haskell (defunctorization) could be used here also. Btw, is there
something equivalent to Obj.magic in SML ?

Ada (or any other imperative language) is indeed a different story.
It's not that functional code is impossible to convert into imperative one :
for instance ocamlopt precisely performs a caml --> asm transformation.
But this transformation is highly complex, and should be left to dedicated
tools. If you really want to make extracted code interact with some
ADA/C/... code, you should rather consider some sort of multi-language
interfacing such as described here: 

http://caml.inria.fr/pub/docs/manual-ocaml/manual032.html

Finally concerning the question of a semantical API to talk to the extraction,
that's something I'm planning to do someday : the extraction uses a kind of
Mini-ML as internal intermediate representation. It shouldn't be too hard to
provide a dump facility of these Mini-ML terms to whatever xml/json you want.
A few details should be addressed nonetheless, for instance the produced
Mini-ML terms aren't currently 100% the same when targeting different 
languages.

Best regards,

Pierre Letouzey