- Author
- Max (Max's blog)
- Published
- 25 July 2026
- Kind
- Personal blog post, informal explainer with a short proof sketch
- Original
- max-amb.github.io/blog/your_type_checker_may_be_wrong/
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work, Getting good
What it is
Max wrote this on a personal blog. It introduces how proof assistants use types to check proofs. It then argues that these checkers are necessarily incomplete.
What it says
- Under Curry-Howard, returning a proof of a fact means returning a value of a type.
- Logical 'and' becomes a pair of proofs, and implication becomes a function between proof types.
- Languages like Lean restrict recursion so that every check finishes in finite time.
- A language that could settle every statement would solve the halting problem.
- The post says a checker is incomplete, not wrong. It may reject correct code but never accepts incorrect code.
- The post concludes that the halting problem implies Godel's first incompleteness theorem.
What evidence it gives
The post offers a proof by contradiction from Turing's halting problem. It also gives one small Lean theorem, proved step by step. It cites Wikipedia and a few other pages. It has no experiments.
Interests and limits
This is a personal explainer with no stated review. The author says it uses intuition and sacrifices some rigour. The Rust recursion limit example is a joke about practice. The halting-to-incompleteness claim is stated in one paragraph. The post does not discuss checking specifications.