[skybrian]

Yes, nonstandard models of arithmetic are what I was thinking of. I don't know much about them, but here is my intuition:

It's a bit odd to think that nearly all "natural" numbers are so large that we can never calculate them, even in principle (because it would take more bits than exist in the universe). Even constructive proofs can describe calculations that could never actually be carried out. The boundary between what I might call "practical" numbers and the larger natural numbers is fuzzy (since it depends on technology), but maybe admitting transfinite numbers exist among the very large naturals would be a way of dealing with it? A way of saying "induction takes us beyond anything we can really know; here be dragons".

And similarly, there are programs that in practice would never halt (because not enough time in the universe), even though theoretically they do.

I don't suppose that's very useful, though, so nice to know it can be avoided.