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.
- GroksBarnacles
Anyone else having the text squeezed to only ~1/3 the page width? On mobile
Edit: Switched to desktop site, and.. that's just how it is
- max-amb
Feel free to ask any questions etc. here :)
- cyanregiment
Oh that's where "currying" comes from?
I thought it was just a delicious way to bind events.