No general procedure can decide whether an arbitrary program will finish, so some well-posed questions have no algorithm at all.
Turing's 1936 proof by diagonalisation. Its practical descendants are everywhere: no general tool can decide whether arbitrary code terminates, so static analysis is always partial.
In practice
- No general tool can tell a developer whether an arbitrary script will terminate, which is why every linter is an approximation.
- A compliance system that tries to decide in advance whether every possible use of a platform is permitted is attempting something no procedure can complete.
- Further reading
- Wikipedia
- Subject
- Technology & Software
- Essay
- The curves, the limits and the laws of software