The Coq mailing list

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

----- Mail original -----
> Thanks to you both for your comments. It hadn't occurred to me to use
> a front end to filter out bad contexts. Is this what normally
> happens in practice?
> 
> I'd be grateful if someone would point me to a non-trivial example of
> an extracted function that has been packaged up in this or some
> other way. Thanks.
> 
> Regards,
> Jeff.
> 


Just a complement to the other answers: indeed, when you extract a function
that has some preconditions, you'll obtain code that may well be abused.
It's your responsibility as user of this code to give it sensible inputs,
i.e. inputs that fulfill the preconditions. If not, you can get answers
that do not satisfy your post-conditions (garbage in, garbage out) ... if you
get any answers at all : your extracted code may enter an infinite loop
on bad inputs, or even crash in flames (up to segfault issues if you played
too much with dependent types).

The only guarantee I provide concerns legitimate inputs : if your input could
be mimicked in Coq, and in Coq you could prove the preconditions on it, then
the extracted code will behave nicely, i.e. simulates the Coq-side 
computations,
hence a) terminates b) on a result fulfilling the post-conditions.
Of course, as in all contracts, there's many nasty lines written in small 
font:
here they concern the lack of surrounding incorrect axioms in your session
of Coq, or any manually extracted code via Extract Constant or similar.

Personally, I tend to avoid as much as possible placing preconditions in the
main functions of a development, the ones the user will play with. For 
internal
functions, that's of course a different story. Another approach is indeed to
design wrappers as suggested by Cédric (either in coq or after extraction).
We could even try someday to provide an extension of the extraction creating
such wrappers automatically, or converting the precondition into runtime tests
(via ocaml's assert for instance). But:
 - you'll need then to have a computable version of your precondition
 - these tests may be costly, and most of them will be useless, typically on
   all inner function calls, where it's the job of the extraction to ensure
   everything will be alright.

A final note : in fact, no need of preconditions to start abusing an
extracted function. Simply create an infinite value in ocaml, for instance
"let rec huge : nat = S huge", and feed it to an extracted recursive function
such as "plus". Game over, this "certified" function will nonetheless never
terminate on this input. However, this doesn't invalidate my correctness
statement above, since "huge" will be impossible to mimick in Coq.
Some of you (I won't give names ;-) are even taking advantage of that
to obtain back arbitrary recursive functions after extraction from
coq functions with explicit nat counter. Clever!

Best regards,
Pierre Letouzey