3 ms·
> This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is no
by hwayne 9y ago
> This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world.
How about, say, a video game? That's something where we reasonably _want_ it to not terminate, because we're primarily interested in its side effects.
- tom_mellior 9y agoThat's what the escape hatches are for. In Coq, for instance, you can also write functions processing infinite streams, provided that they also produce something regularly. For example, in a game, you could write a function from an infinite stream of inputs to an infinite stream of frame updates. You can not write functions that would not terminate while computing the updates for some given frame. Alternatively, you just write a function to iterate your game world update N times, where you choose N large enough to ensure that your game can run until the heat death of the universe. That's not a nonterminating function, but it's long-running enough for all practical purposes.