3 ms·
It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning. It's also useful because,
by creata 6y ago
It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning.
It's also useful because, in practice, we don't accidentally write code that "obviously terminates but not in the lifetime of this universe" as often as we accidentally write nonterminating code, so a lot of mistakes can still be caught by termination checking.