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