Good point; I guess I was thinking of the simplified textbook case of computations with no external interaction. I wonder if this MIT system is able to exclude the most likely false positives, like polling for input? On the other hand, maybe polling too long for input counts as an infinite---or at least, too long---loop for their use-case of interrupting user programs that seem to be hanging, so that the user can save.