Computability
Computability in Practice
'Why did my linter miss this bug? Why does the Rust compiler reject my code?' - both questions have one answer: Rice's theorem. The fundamental limits of computability determine what the tooling of every developer can and cannot do.
- Rust borrow checker: sound analysis grounded in type theory
- ESLint/Pylint: incomplete static analysis with false positives
- Formal verification (Coq): mathematical proofs of code correctness
- TypeScript: intentionally unsound for developer convenience
Rice's Theorem: The Limits of Static Analysis
**Rice's Theorem:** Every non-trivial semantic property of programs is undecidable. This means: no algorithm can correctly answer, for every program P, whether P has a given property (other than trivial 'always yes' / 'always no').
**Implication for developers:** Static analyzers (ESLint, PMD, Coverity) use approximations - either sound (no false negatives, but false positives possible) or complete (no false positives, but may miss bugs). Perfect precision is unachievable.
Why can't static analyzers precisely detect all memory leaks?
The Halting Problem in Real Systems
Despite being undecidable in general, **approximate solutions** work extremely well in practice. Real systems use restricted domains or heuristics.
**Coq and program proofs:** In Coq you can't write an unchecked function - all functions must terminate. This makes Coq sub-Turing-complete, but all proofs are correct. The tradeoff: expressiveness vs guarantees.
Why does the Rust borrow checker sometimes reject valid code?
Type Systems and Their Expressiveness
The **expressiveness hierarchy** of type systems is directly linked to computability. The more expressive the system, the harder (or impossible) type inference becomes.
**Practical takeaway:** TypeScript is intentionally unsound - 'any' and type assertions let you bypass the type checker. Flow (from Facebook) is also unsound. Full type correctness at the cost of convenience is Haskell's choice.
The more expressive the type system, the better the language: more bugs caught at compile time, more invariants verified.
Type system expressiveness runs directly into undecidability of type inference. Dependent types and System F-omega make inference undecidable (or exponential), so industrial languages (Rust, TypeScript) deliberately trade power for automatic inference.
The intuition "more types means safer code" is correct for bugs but ignores the cost: Haskell type inference is decidable, while Coq/Agda require manual proofs. TypeScript is intentionally unsound (any, type assertions) precisely because a sound version would make compilation impossible on large codebases. Computability sets a hard ceiling above engineering preferences.
Why is type inference undecidable in System F?
Key Takeaways
- Rice's Theorem: every non-trivial semantic property of programs is undecidable
- Static analyzers: either sound (false positives) or complete (false negatives)
- Type system hierarchy: expressiveness ↑ → inference decidability ↓
- Hindley-Milner: golden balance - full type inference and Turing-completeness
- Dependent types: maximum expressiveness, non-termination is forbidden
Related Topics
Practical application of computability theory.
- Undecidability — Rice's theorem extends undecidability results
- Reductions — Proofs via reduction to the Halting Problem
Вопросы для размышления
- Can you design a programming language where all programs are guaranteed to terminate? What would be the cost?
- Why does Google use Abseil (C++) instead of formal verification for critical code?
- How does Rice's theorem explain why a perfect antivirus is impossible?
Связанные уроки
- comp-09 — Undecidability - the theoretical foundation for practical limits
- comp-12 — Reduction shows which practical problems are undecidable
- cplx-07 — NP-hard problems: practical limits analogous to undecidability
- alg-22-backtracking — When a verifier exists - NP; when it doesn't - undecidability
- cplx-01