&gt; For most tasks we can restrict ourselves to a terminating subset without bottom. See Agda, Coq, Isabelle, etc.<p>While those are interesting languages, I kind of was under the impression that they were generally <i>not</i> seen as suitable for &quot;most tasks&quot;.