Re: A bit further toward the flamewar

[Ludovic Courtès]

Howdy,

address@hidden skribis:

> but I
> understand that you could be very interested in Coq proving that a
> complex recursive algorithm eventually terminates, while you don't care
> much about the type checking.

Actually, I just meant to say that type-checking is one of the many
checks one may want the compiler to perform automatically.

Ludo’.