Reference. The formulae-as-types notion of construction [howard-80]

1980
William Alvin Howard
To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism

Backlinks

Against Curry-Howard Mysticism [loc-000S]

May 25, 2025
Liam O'Connor

As someone who teaches PL theory and has worked in PL theory for many years now, I love the the formulae-as-types notion of construction, also known as the Curry-Howard correspondence. It demonstrates a profound connection between lambda calculi and logic. Wadler's paper and accompanying talk provide an approachable introduction to the topic.

Yet, among the audience for such talks (which are primarily geared at functional programming practitioners rather than academics) are many who, I think, are getting the wrong message somehow. I see muddled, severely distorted, or even outright untrue claims being made about type theory and Curry-Howard quite frequently as a result of these misconceptions. So, to clear the air, I'll state my thesis up-front:

Thesis.

May 25, 2025
Liam O'Connor

For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.

Learn it if you want, but it will not and cannot aid you in improving your programming practice (unless you're writing Idris or Lean!).

The Curry-Howard correspondence says that types correspond to propositions (or formulae) and programs that inhabit these types correspond to proofs of their respective propositions. So, programs are proofs, yes, but proofs about what?. Certainly not the programs themselves — without a dependently-typed language, we can't state propositions about programs on the type level. For most standard type systems, our propositions take the form of abstract logical sentences in a fairly limited (and inconsistent) propositional or second order logic, not theorems about programs.

But I get theorems from the types!

May 25, 2025
Liam O'Connor

It is true, however, that we learn many theorems about our programs from examining their types. From the judgement $f : \texttt {Int} \rightarrow \texttt {Bool}$ , I know that the function $f$ will, when executed with an $\texttt {Int}$ argument, produce a $\texttt {Bool}$ result. This is indeed a theorem! But it is not a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of type safety. A similar argument applies when types are used as "witnesses" of a property, e.g. $\textit {balance} : \texttt {Tree} \rightarrow \texttt {BalancedTree}$ If $\textit {balance}$ is the only way to produce a $\texttt {BalancedTree}$ , then one might be tempted to say that this type "corresponds" to a proposition that a tree is balanced. But this is not a theorem that follows from formulae-as-types but rather from good ol' type safety and enforcement of module boundaries, just as above.

The theorems for free also popularised by Wadler, specifically the theorems obtained from the generality of a type signature, are also not a consequence of Curry-Howard, but rather a consequence of the parametricity of the type system.

Furthermore, type isomorphisms (for example, $(a + b) \times c \simeq a \times c + b \times c$ ), which can be used to simplify programs, are also not a consequence of Curry-Howard. The analogous logical statement that $(a \lor b) \land c \Leftrightarrow a \land c \lor b \land c$ is true, sure, but so is $\texttt {Int} \Leftrightarrow \texttt {Bool}$ . In a simply typed programming language, nearly all useful types ( $\texttt {Int}, \texttt {\texttt {Bool}}$ etc.) will be logically equivalent to just $\texttt {True}$ , so such propositional equivalence is much too weak. Such isomorphisms are between semantic domains (covered in detail in my domain theory notes) — the meanings of types, not their logical analogues.

Why does this happen?

May 25, 2025
Liam O'Connor

Many programmers can get swept up in mysticism about Curry-Howard, overstating its consequences. Of these, I think there are two main groups: the mathematically curious and the mathematical fetishists. The curious are those who, usually through no fault of their own, have no or little experience with program specification, verification, formal methods, semantics, proofs etc, before being introduced to Curry-Howard. They then make the mistake of thinking that Curry-Howard is central to all of these new areas to them, simply because it was their starting point. To a certain extent, I do understand this viewpoint — being excited about a particular topic in research is a good thing! The good thing here, is that this problem can be resolved simply by doing better education, so that programmers' first exposure to logic, for example, isn't in third year university, when puzzling out types for lambda calculus terms.

Far more problematic, though, is the culture of mathematical fetishism within the functional programming community: the use of mathematical jargon to obscure rather than clarify — to show superiority over others, rather than establishing a common vocabulary. One example of this is those who insist on calling the Curry-Howard correspondence "the Curry-Howard isomorphism" because it uses an exclusively mathematical term, "isomorphism", rather than the more commonly-used (and more accurate) "correspondence". They will often talk very confidently, using large amounts of mathematical jargon, where in reality the idea under discussion is either significantly more straightforward than indicated, or outright wrong. People who behave in this way are really toxic for a programming community. The only solution I can recommend is to try hard to exclude this kind of toxic behaviour from programming communities, and to devote resources to supporting those learners who would otherwise potentially be led astray by this kind of behaviour.