##6 Conclusion and future works

Coq extraction is hence a rich framework allowing to obtain certied programs
expressed in Ocaml, Haskell or Scheme out of Coq developments. Even if some
details can still be improved, it is already quite mature, as suggested by the variety
of examples mentioned above. This framework only seems to reach its limit
when one tries to discover algorithm buried in large mathematical development
such as CoRN, or when one seeks a ne control a la Minlog on the elimination
performed by extraction. Most of the time, the Prop/Set distinction, which is
a rather simple type-based elimination criterion, is quite ecient at producing
reasonable extracted terms with little guidance by the user. Moreover, new tools
such as Russel or Function now allow to easily dene general recursive functions
in Coq, hence allowing a wider audience to play with extraction of non-trivial
Coq objects.

The correctness of this extraction framework currently rely on the theoretical
studies made in [7](Reference#section-7), [8](Reference#section-8). The next perspective is to obtain a mechanically-checked
guarantee of this correctness. Work on this topic has already started with a
student, S. Glondu. Starting from B. Barras CCI-in-Coq development, he has
already dened a theoretical extraction in this framework and proved one of the
main theorem of [7](Reference#section-7). Another interesting approach currently under investigation
is to use a Coq-encoded Mini-ML syntax as output of the current uncertied
extraction, and have an additional mechanism try to build a proof of semantic
preservation for each run of this extraction. Such extracted terms expressed in
Mini-ML could then be fed to the certied ML compiler which is currently being
built in the CompCert project of X. Leroy.

Some additional work can also be done concerning the typing of extracted
code. For instance, thanks to advanced typing aspects of Haskell and/or Ocaml,
examples such as the existential structure aMonoid may be typed some day
without unsafe type casts. This would help getting some sensible program out of
CoRN, which make extensive use of such structures. Manual experiments seem to
show that Ocaml object-oriented features may help in this prospect. At the same
time, some preliminary work has started in Coq in order to propose Haskell-like
type classes, adding a support for these type classes to the Haskell extraction
may help compensating the lack of module and functor extraction to Haskell.