Re: A bit further toward the flamewar

[rixed]

> 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.

It's funny how researchers are concerned by proofs that a program
terminates, while most engineers try hard everyday to design programs so
that they never terminates (unexpectedly). :)

I realize we merely don't work in the same fields.  I always write
trivial softwares that handle complex data structures and internal
states, while you probably, both as a researcher and a guile hacker, are
more used to write complex softwares manipulating in non-trivial ways
mere lists of symbols.

So I'm very interested in static type checking while, for instance,
I never fear that one of my simple for-loop may not terminate ; 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.