The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Fri, Nov 07, 2008 at 02:32:59PM +0100, Stéphane Lescuyer wrote:
> Well, extraction is indeed tagged as 'experimental' in the
> documentation, but it would agree with you nonetheless. I am actually
> using extraction on a rather big Coq project and it works perfectly
> (except a couple of glitches that were corrected by Pierre anyway).
> 
> Stéphane
> 
> On Fri, Nov 7, 2008 at 2:15 PM, Adam Chlipala 
>Â <adamc AT hcoop.net>
>  wrote:
> > AUGER Cédric wrote:
> >>
> >> Extraction is still experimental
> >
> > Really?  I've been thinking of it as one of the most core, 
> > well-established
> > features of Coq.  I've used it since 7.something.
> >
> > Is there some new reimplementation that might have introduced regression
> > bugs?
> >

Ok, let me elaborate a bit about this "experimental" status of the
extraction.

The quick answer is : don't worry, the extraction _is_ reliable, at
least as much as most other parts of Coq (or maybe I should rather say
that the rest of Coq isn't particularly less experimental than
extraction ;-)

The warning at the top of the documentation was added (or kept, I
don't remember) when Coq started to be distributed with the
reimplementation of the extraction I've done during my PhD (early Coq
7.x, around year 2000). At that moment, both the extraction code and
the theory behind it were clearly work-in-progress, usable but
evolving quickly and potentially broken. Around 2004, some progress
was made concerning the theory (see my thesis). Since then the core of
the extraction hasn't moved much and has proved to be quite robust:
over the recent period, I can remember of only one bug resulting in
wrong answer when executing extracted code (#1128, march 2006). It's
not perfect though, as mentionned by Stéphane there are still a few
rare glitches, mostly in the context of non-trivial modules, but they
aren't too critical in the sense that faulty extracted code is
hopefully detected and rejected by the ocaml/haskell type-checker.
Many difficulties were related to the semantics of functor and naming
and scoping conventions of Coq vs. Caml. These kind of issues are
slowly being addressed. See for instance bugs #1526, #1895, or #1914
(I'll close the last one later today, Coq 8.2 will include this
fix). At the same time, there remains a few situations that I
currently don't really know how to handle in a satisfactory manner :
see #843 or #1957. In these situations, extracted code is correct
execution-wise but not ML-typable.

So, why is the extraction still marked as experimental in the
documentation ? Multiple possible answers, pick yours:
a) I haven't browsed the documentation of my own tool for a long long 
time, and hence haven't updated it (after all, except from the warning,
it's reasonably accurate)
b) I'm a chicken afraid to advertise my code as rock-solid
c) I would like to see #843 and #1957 solved before declaring the
end of the experimental phase.
d) For the extraction to be completely trustworthy, it would be nice
to either certify it in Coq, or make it output proof-certificates
alongside extracted objects. Stéphane Glondu is currently working 
on that with me.

Best regards,
Pierre Letouzey