Ron Pressler’s extended 2016 talk traces the difficulty of software correctness to the nature of computation. Some questions about arbitrary programs cannot be decided by a general algorithm; others are decidable but too expensive to check in the worst case.
His tour connects those limits to engineering practice:
- Interactions expand the problem. Even when individual components are understood, their combined behavior can be difficult to verify. A finite system can still have an enormous number of possible states.
- Verification methods trade scope for cost. Model checking explores a system model; deductive proof can require substantial human work; static analysis simplifies behavior and may give an inconclusive answer.
- Types check particular properties. They can rule out important categories of error without establishing every behavior a system needs.
Pressler calls for studying real failures to decide where to spend verification effort. Memory safety and error handling are examples of properties worth investigating because their failures can be costly.
The theoretical limits concern general solutions, not a verdict on every project. A focused model, test, or proof can still provide valuable assurance about the behavior that matters most.