> A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience.

Nontermination alone isn't enough, since in some provably-terminating languages it's still very possible to write expressions that will take a very long time to evaluate in some implementations. Concretely, "catastrophic backtracking" regular expressions can be true regular expressions (and therefore provably terminating), but in naive implementations their runtime will be exponential in the input length.

But it's a start, and the same techniques could hopefully lead to languages in which expressions naturally come with upper bounds on their evaluation time.