Total Functional Programming [pdf]
The focus on &quot;totality&quot; undersells one key advantage of the restrictions in this language. You gain the ability to easily prove general properties about your program. This is <i>not</i> a consequence of totality. There are total programming languages which allow you to write programs with undecidable properties. This is really a language where properties are easy to prove, and termination happens to be one of them.<p>The topic often comes up in the discussion of smart contracts on public blockchains, and people often get confused about what Rice&#x27;s theorem says. I recently did a small write up on the topic (plug, plug)<p><a href="https:&#x2F;&#x2F;hackernoon.com&#x2F;smart-contracts-turing-completeness-reality-3eb897996621#.heipbfzgf" rel="nofollow">https:&#x2F;&#x2F;hackernoon.com&#x2F;smart-contracts-turing-completeness-r...</a>