Proofs as Programs - by InputName
Systems Thinking Collection
SubscribeSign in
Logic<br>Proofs as Programs<br>From Curry-Howard to a Deal with the Devil and the Future of Mathematics<br>Jun 01, 2026
Share
Dependency Graph for Liquid Tensor Experiment - Xenaproject<br>A short disclaimer before we begin. I am very much a student of this subject, and this essay reflects my current understanding—including the edges where that understanding is still forming. Mathematicians talk a lot about intuition, yet their texts often feel designed to prioritize rigor over teaching. I believe there is value in an essay that could conceivably be read in an hour, serving as a companion before, during, or after the formal learning process. Finally, writing this was an exercise in the Feynman technique; I built this essay as a personal tool to make myself understand the material. Interspersed within this essay is some of my cognitive scaffolding that a more experienced student might have torn down. Perhaps it will be of use.<br>I. The History of the Curry-Howard Correspondence
(https://en.wikipedia.org/wiki/Curry%E2%80%93Howard*correspondence)<br>The beginnings of the Curry–Howard correspondence lie in several observations:<br>In 1934, Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.<br>In 1958, he observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment with the typed fragment of a standard model of computation known as combinatory logic.<br>In 1969 Howard observes that another, more high-level proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus.
I-1. Combinators - SKI
Well that is a lot of words that I don’t know much about. Lets break it down.<br>Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.<br>Combinators : Functions that move data around. They have no free variables and thus can only be aware of what is handed to them.
Types : In programming, a type tells you what kind of data you are working with (e.g., an integer, a string, or a function that turns an integer into a string)
Intuitionistic Logic : Logic that requires you to build an example to prove something is true. Most notably you can’t prove by contradiction (apply the Law of Excluded Middle)
Curry noticed if you look at the types of those basic programming building blocks, they look exactly like the axioms used by mathematicians to build logical proofs.
This still feels to free floating. Let’s see what ‘types of the combinators could be seen as axiom-schemes’ actually means<br>We begin with the Identity Combinator, the I Combinator. It takes x and returns x
\(A \rightarrow A\)
Next we look at the Constant Combinator, the K Combinator that takes a first input, then a second input. It ignores the second input and returns only the first input.<br>\(A \rightarrow (B \rightarrow A)\)
You can take a moment to stop and check that this indeed is the correct form of the function. Instead of taking both inputs as the same time, after taking the first input we return a function that takes a second input.<br>Now constructing the S combinator would require a bit of work. But I will state it’s form here.<br>\((A \rightarrow (B \rightarrow C)) \rightarrow ((A\rightarrow B) \rightarrow (A \rightarrow C))\)
To begin breaking down the S combinator , notice that for all its complexity you can begin reading it from the middle arrow. It takes a function and yields another function, where the latter distributes A to B and C.<br>If we read the arrows as implies we recover Hilbert’s Axiom System for Propositional Logic, or a fragment of it as we can only recreate the parts that can be written with arrows (pure implication).<br>This clarifies what the Implicational part of Intuitionistic Implicational logic means. It’s the part with arrows.<br>Nice.<br>I-2. SKK = I
Moving from 1934 to 1958.<br>Curry observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment with the typed fragment of a standard model of computation known as combinatory logic.<br>Hilbert-style deduction system: A way of writing out mathematical proofs step-by-step. Notorious for being clunky to write.
Combinatory Logic: A mathematical model of how computers calculate things built using combinators.
Curry realized the structure of a Hilbert-style proof was identical to the structure of a typed program written in combinatory logic.
The most famous example of the Curry-Howard correspondence at this level is the Identity function (proving that A implies A).<br>Both the logician and the programmer are restricted to using only two tools. We have however, already defined these.<br>The K Combinator / Axiom 1:
\(A \rightarrow (B \rightarrow A)\)
The S Combinator / Axiom 2:
\((A...