- Type checkers underpin proof assistants like Lean and Rocq, enabling verification of mathematical proofs through the Curry-Howard correspondence.
- The Curry-Howard correspondence maps logical operations to type constructs: conjunction to product types, implication to function types, etc.
- Proof assistants validate proofs by checking that a program returns the correct type, but this requires the program to terminate.
- The halting problem (undecidable) means type checkers cannot always determine if a program terminates, leading to incompleteness.
- Formal languages restrict recursion to ensure termination, but this makes them unable to prove or disprove all statements (Gödel's first incompleteness theorem).
- The halting problem implies Gödel's incompleteness theorem via the Curry-Howard correspondence, showing type checkers are provably imperfect.
- Consequently, type checkers may reject correct code (though never accept incorrect code), so they can be 'wrong' in the sense of incompleteness.