The Coq mailing list

[Arnaud Spiwack <arnaud.spiwack AT gmail.com>]

> ay this is not too important, if one agrees that the
> "no-check" option is really unsafe and for experimentation.
> Whether this option should be offered and documented in
> the standard Coq is however a question I would not decide
> alone.
The idea, at this point of discussion was to have an "Unsafe Fixpoint" 
keyword, or a "{ unsafe }" guard condition, to allow to define non 
structurally terminating functions. Which is somewhat similar to adding 
an axiom. It can lead to inconsistencies, but so can axioms. It can lead 
to diverging typechecking, but paraphrasing Thorsten Altenkirch on this 
one, there is little difference between diverging and answering "no".

If it can actually lead to segfault (no time to check today, but that 
could be fun) it might be more annoying but not overly troublesome. That 
would very much make it the "Obj.magic" of Coq.


Arnaud Spiwack