Why Your Type Checker May Be Wrong: Lean and the Curry-Howard Correspondence
An introduction to formal proof verification and the Curry-Howard Correspondence
I explore how proof assistants like Lean leverage the Curry-Howard correspondence to treat mathematical proofs as computer programs. By mapping logical operations to types, these tools verify complex theorems automatically. However, I reveal a critical limitation: if a proof involves non-terminating expressions, the type checker cannot definitively validate the result, meaning it might be wrong even when you believe you are right.
Therefore, one may be surprised by the fact that type checkers also form the backbone of proof assistants, which may mean your type checker is wrong or just may not know you are right.