Re: A bit further toward the flamewar

[Ludovic Courtès]

Hans Aberg <address@hidden> skribis:

> On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:
>
>> Did you know that Coq would only compile a function when it can prove
>> that it terminates?  That’s another kind of compiler-supported proof one
>> quickly gets used to.
>
> Termination is a non-deducable property. They look at a intuitionistic subset 
> of programs.

Sorry, I’m not sure what you mean.

What I had in mind is what they call “well-founded recursion” [0] and
the idea that a recursive function must have a “decreasing argument” [1].

Thanks,
Ludo’.

[0] http://coq.inria.fr/refman/Reference-Manual005.html#htoc79
[1] http://coq.inria.fr/refman/Reference-Manual003.html#Fixpoint