A program that enumerates all theorems in ZFC and stops when it proves a contradiction (e.g. true = false). Encoding a program that is equivalent to that directly as a Turing Machine in merely 748 states: https://www.scottaaronson.com/papers/bb.pdf (meaning that we cannot prove an upper bound on the 748th Busy-Beaver number, but there are probably even smaller undecidable TMs).
But my favourite example (shown here in Java) demonstrates the difficulty of analysing simple, realistic programs without necessarily being undecidable:
long foo(long x) {
if (x <= 2 || (x & 1) != 0)
return 0;
for (var i = x; i > 0; i--)
if (bar(i) && bar(x - i))
return i;
throw new Error();
}
boolean bar(long x) {
for (var i = x - 1; i >= 2; i--)
for (var s = x; s >= 0; s -= i)
if (s == 0)
return false;
return true;
}
Even in this case where even the input space is finite (and so everything here is definitely decidable), we simply don't yet know whether there is some x for which foo(x) throws, let alone if we made the input unbounded by using BigInteger instead of long.
A program that enumerates all theorems in ZFC and stops when it proves a contradiction (e.g. true = false). Encoding a program that is equivalent to that directly as a Turing Machine in merely 748 states: https://www.scottaaronson.com/papers/bb.pdf (meaning that we cannot prove an upper bound on the 748th Busy-Beaver number, but there are probably even smaller undecidable TMs).
But my favourite example (shown here in Java) demonstrates the difficulty of analysing simple, realistic programs without necessarily being undecidable:
Even in this case where even the input space is finite (and so everything here is definitely decidable), we simply don't yet know whether there is some x for which foo(x) throws, let alone if we made the input unbounded by using BigInteger instead of long.