[eru]

For most tasks we can restrict ourselves to a terminating subset without bottom. See Agda, Coq, Isabelle, etc.

[eli_gottlieb]

Bingo. But most people also like to kvetch and moan about the restrictions imposed by programming with only structural recursion and productive corecursion -- even though those are usually exactly what we want.

[eru]

Especially if you get an easy way out for when you need it.

Like unsafePerformIO, but for calling not-proven-to-be-terminating functions. Or an explicit marker like the wrapping monads for side-effecting functions.

[dragonwriter]

> For most tasks we can restrict ourselves to a terminating subset without bottom. See Agda, Coq, Isabelle, etc.

While those are interesting languages, I kind of was under the impression that they were generally not seen as suitable for "most tasks".

[eru]

I mean, even in Haskell, big chunks of every program can be automatically recognized as `safe Haskell'.