Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence | Max's blogYour type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence<br>25 Jul, 2026<br>ContentsWhen writing code many of us have been saved time and time again by type checkers: the useful piece of software that ensures you aren&rsquo;t adding a string to an integer 1 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&mldr;<br>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.<br>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).<br>The Curry-Howard correspondence<br>A light definition of the Curry-Howard (CH) correspondence could be:<br>proofs can be represented as programs, (&mldr;), proofs can be run2

This definition certainly doesn&rsquo;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?<br>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&rsquo;t strictly correct, but it is enough for the purposes of this post.<br>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$.<br>To seriously work with our new proof object, we must first translate a few logical operations from propositional and predicate logic to our new paradigm. We begin with the most simple:<br>$$<br>X \text{ is true}<br>$$In our case, for $X$ to be true, we must have a proof of $X$, i.e.<br>$$<br>\exists p : p \in P(X)<br>$$The way we say this is: $P(X)$ is inhabited 3. For example, $P(5=5)$ is inhabited but $P(5+2=6)$ is not (as there is no proof of this in peano arithmetic, it is false).<br>The next logical operation to represent is &ldquo;and&rdquo; ($\wedge$). For those unfamiliar, we have $X \wedge Y$ if and only if both $X$ and $Y$ are true. So we have that both $P(X)$ and $P(Y)$ are inhabited, i.e. $\exists p: p \in P(X)$ and $\exists p\prime : p\prime \in P(Y)$. This means we can construct an object $(p, p\prime)$, so we have that<br>$$<br>P(X) \times P(Y)<br>$$(where $\times$ represents the cartesian product) is inhabited ($(p, p\prime) \in P(X) \times P(Y)$).<br>Next, we want to represent the implication operation. If $X \implies Y$ then either $X$ is false, or $X$ is true and $Y$ is true. We represent this as the existence of a function from $P(X)$ to $P(Y)$:<br>$$<br>P(X) \to P(Y)<br>$$If this function exists, then whenever we have a proof of $X$, we can derive a proof of $Y$. If $X$ is false (so $P(X)$ is not inhabited), then the function does not have its input, so $P(Y)$ may or may not hold.<br>In the interests of conciseness, I omit discussions about the rest of the standard logical operations. They translate to set theory like so (but are not relevant for the remainder of the post):<br>Logical operationSet theory$X \lor Y$$P(X) + P(Y)$ (Where $+$ represents a disjoint union)$(\forall(n \in \mathbb{N})X(n))$$(n: \mathbb{N}) \to P(X(n))$$(\exists(n \in \mathbb{N})X(N))$$(n: \mathbb{N}) \times P(X(n))$4How do proof assistants use the CH correspondence<br>Proof assistants use this correspondence and their type checkers to validate proofs. But how do they do this? To show how, let us prove a simple theorem using lean notation.<br>A theorem<br>Consider the below theorem named blog:<br>theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z

It begins by stating that $X, Y$ and $Z$ are logical statements, i.e. they are things that may or may not be true. This is like constructing the sets $P(X), P(Y)$ and $P(Z)$, but not saying if they are inhabited yet.<br>Next we have a hypothesis, $h_1 : X$, which serves as a proof of $X$. Thinking back to our earlier discussion, you may remember that having a proof of $X$, is equivalent to $X$ being true, so $h_1 : X$ simply gives, $X$ is true. This is similar with $h_2$, but $h_2$ gives a proof of $Y$.<br>Then we have final hypothesis, which using unbounded creativity...