I’ve seen this come up around the halting problem too.
The novice encounters a problem where a halting oracle would be useful, and says, “Oops, I guess this whole problem is just impossible; everyone knows halting is undecidable.” But —
It’s true that you can’t write a program that will accept an arbitrary program P as input and tell whether P will halt. You certainly can, though, write a program that will tell whether a very broad set of useful programs will halt, and reject any that can’t be shown to halt.
Sometimes what you want isn’t to evaluate whether an arbitrary program will halt, but to alter an arbitrary program into one that definitely halts — for instance by applying a resource limit that will halt the program if it keeps running too long.
If you’re providing a language for untrusted users to submit programs, maybe you don’t need looping or recursion at all! For example, the Sieve language for email filters does not support looping. Or you might need finite looping but not unbounded looping: a foreach loop over a materialized list, but not a while loop on a boolean condition.
More generally: The theorem tells you about the general case, but you probably don’t live in the general case.
As an aside: yes, SRE is a rationality practice. And a lot of the interesting parts of it are group rationality practice, too.
Even if there’s a sophisticated and more accurate way of describing the problem space, practicality can often push you back to a more general description with an extra hacky constraint (resource limits) shoved on top.
I’ve seen this come up around the halting problem too.
The novice encounters a problem where a halting oracle would be useful, and says, “Oops, I guess this whole problem is just impossible; everyone knows halting is undecidable.” But —
It’s true that you can’t write a program that will accept an arbitrary program P as input and tell whether P will halt. You certainly can, though, write a program that will tell whether a very broad set of useful programs will halt, and reject any that can’t be shown to halt.
Sometimes what you want isn’t to evaluate whether an arbitrary program will halt, but to alter an arbitrary program into one that definitely halts — for instance by applying a resource limit that will halt the program if it keeps running too long.
If you’re providing a language for untrusted users to submit programs, maybe you don’t need looping or recursion at all! For example, the Sieve language for email filters does not support looping. Or you might need finite looping but not unbounded looping: a foreach loop over a materialized list, but not a while loop on a boolean condition.
More generally: The theorem tells you about the general case, but you probably don’t live in the general case.
As an aside: yes, SRE is a rationality practice. And a lot of the interesting parts of it are group rationality practice, too.
This is getting a bit into the weeds, but I find that this blog post mirrors my experience with Turing incomplete languages: https://neilmitchell.blogspot.com/2020/11/turing-incomplete-languages.html?m=1 (it also has the advantage of talking about a language that I’ve used in industry, and can personally attest to a little).
Even if there’s a sophisticated and more accurate way of describing the problem space, practicality can often push you back to a more general description with an extra hacky constraint (resource limits) shoved on top.