It Doesn't Work in Theory, but It Is All Right in Practice
I collect historical anecdotes about things that were impossible from a theoretical point of view, yet turned out to be quite achievable, and useful, in practice.
There is a widespread belief that you cannot write a program that finds all the bugs in other programs. John MacCormick, in What Can Be Computed?, gives "finding all bugs" as a textbook example of an uncomputable problem: not computable in theory, and not in practice.John MacCormick. What Can Be Computed? A Practical Guide to the Theory of Computation. Princeton University Press, 2018. From theory, this is absolutely true. It is proven that no such program can be built, neither today nor in the future.
However, this is only partially true in reality. What was actually proven is narrower: there is no way to predict whether an arbitrary program halts on a given input by looking only at its source code, for every possible program. In fact, programs that find bugs are not only possible to write; they already exist.
| Category | What it means |
|---|---|
| Tractable | Computable in theory and in practice. |
| Intractable | Computable in theory, but with no effective algorithm in practice (yet). |
| Uncomputable | Not computable in theory or in practice. Ever. |
A note from my "personal Google" holds two quotes from Communications of the ACM about a tool called Terminator, which can quite often prove that a given program halts for any given input. "Quite often" here means often enough to be used in practice, at Microsoft.
It doesn't work in theory, but it is all right in practice.the recurring shape of these anecdotes
Do you have other examples? I would love to hear about them.