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