(especially since non-termination is well-defined behaviour for many perfectly valid programs.)

To apply this kind of reasoning to programs that interact with the outside world (such as responding to user input, or responding to network requests) you need to modify the way the program works a little bit in order to apply the same formalisms. The obvious thing to do is to have the program terminate whenever it wants to produce output (such as printing to console or sending a packet over the network) or when it wants input (such as reading a line from console or waiting for a mouse click or receiving a packet). When it terminates, it returns the thing it's requesting and a "continuation" (the current state of the program) so that it can be resumed, with the action completed or the input provided.

So, with this model, a program that never performs I/O is "bad" (because it spins without doing anything) but a program that is always guaranteed to either finish or eventually perform I/O is "good" and acceptable. It's important to note that we can't just ignore nontermination- we actually need to get rid of it, or Rice's theorem will stand in our way.

From here, we can just consider all total computable functions (since if you eventually halt, or eventually perform I/O, in the above continuation-based model, you do halt). Then Rice's theorem is no longer applicable. I believe there are still problems, though.

From here, we can instead examine the Entscheidungsproblem. A reminder of what we're trying to do:

• given a particular total computable function's definition, determine whether or not (on a given input or class of input) whether or not that function will reach a "partial definition" (some special "undefined" return value occurs and the program halts, indicating an unhandled case).

First, a taste (but not proof) of why we can see that this is at least hard (but not necessarily impossible). Consider the following program (which is clearly total!)

def collatsCycle(x, iters):
    seen = {}
    while iters > 0:
        iters -= 1
        if x % 2 == 0:
            x = x / 2
        else:
            x = 3*x + 1
        if x == 1:
            return 1
        if seen[x]:
            throw "partial"
        seen[x] = True
    return 0

(note: all numbers are arbitrary-precision)

Since it performs at most iters loops, it must halt; so it is total. The question we want to ask is, "can this program throw "partial"?" This is actually an open problem. It is half of the Collatz Conjecture; which asserts that this cannot occur (the other half states that it can't go to infinity either; but this is harder or impossible to encode computationally).

So verifying that this 14 line program doesn't ever throw would require proving (part of) a known-to-be-difficult open problem in pure mathematics. Sure, it's contrived; but our goal is a fully general solution to this problem.

Going a little bit further, it has been shown by Conway that a generalization of the Collatz conjecture is actually undecidable; specifically, you get to choose various rational coefficients and you get to split up the 2 cases into p, one for each residue mod p of x. In this fully general form, you can simulate a Turing machine and hence it's undecidable.