GoKawiil25 Jul, 2026
When writing code many of us have been saved time and time again by type checkers: the useful piece of software that ensures you aren’t adding a string to an integer or returning a reference to a value instead of the owned value. However, while useful, and sometimes annoying, it seems that the humble type checker has limited capability beyond its noble task of saving our asses…
Therefore, one may be surprised by the fact that type checkers also form the backbone of proof assistants - languages like Lean and Rocq. They use the structure gained from types to definitively check whether some statement follows from some other statements - or more colloquially, to verify mathematical proofs.
In this blog I would like to first introduce some of the more basic elements of the Curry-Howard correspondence, followed by how it is used in proof assistants and eventually, why this may mean your type checker is wrong (or just, may not know you are right).
The Curry-Howard correspondence
A light definition of the Curry-Howard (CH) correspondence could be:
proofs can be represented as programs, (…), proofs can be run
This definition certainly doesn’t give much away, however one possible line of thought may derive that as proofs can be represented as programs, we need a way for programs to return proofs. But what does this even mean to return a proof?
Reverting back to fundamentals: in order for a program to return an integer, we say that it returns the type $\text{int}$, which could be any integer. So $\text{int}$ represents the set of integers. Similarly, for a program to return $\text{True}$ or $\text{False}$, we say it returns the type $\text{bool}$, which contains both possibilities. This approximation of types as sets isn’t strictly correct, but it is enough for the purposes of this post.
Attempting to extend this to proofs, one may say that when a program returns a proof of some fact, it returns an element of the type $P(X)$. Where $P(X)$ is the set of all proofs of fact $X$.
... continue reading