my forest
bits and pieces
+30
-4
+4
-3
trees/loc-000S.tree
+4
-3
trees/loc-000S.tree
···
1
1
\import{dt-macros}
2
2
\date{2025-05-25T13:36:39Z}
3
+
\author{liamoc}
3
4
\title{Against Curry-Howard Mysticism}
4
5
\p{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](howard-80), also known as the Curry-Howard correspondence. It demonstrates a profound connection between lambda calculi and logic. [Wadler](wadler)'s [paper](wadler-14) and accompanying [talk](https://www.youtube.com/watch?v=IOiZatlZtGU) provide an approachable introduction to the topic.}
5
-
\p{Yet, among the audience for such talks, 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:}
6
+
\p{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:}
6
7
\thesisblock{
7
8
\p{\strong{For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.}}
8
9
}
···
11
12
\subtree{
12
13
\title{But I get theorems from the types!}
13
14
\p{
14
-
It \strong{is} true, however, that we learn many theorems about our programs from examining thier 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 \strong{not} a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of [type safety](https://en.wikipedia.org/wiki/Type_safety). A similar argument applies when types are used as "witnesses" of a property, e.g. ##{\textit{balance} : \texttt{Tree} \rightarrow \texttt{BalancedTree}}
15
+
It \strong{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 \strong{not} a theorem arrived at by any use of the Curry-Howard correspondence, but rather a straightfoward consequence of [type safety](https://en.wikipedia.org/wiki/Type_safety). A similar argument applies when types are used as "witnesses" of a property, e.g. ##{\textit{balance} : \texttt{Tree} \rightarrow \texttt{BalancedTree}}
15
16
If #{\textit{balance}} is the \em{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 \em{not} a theorem that follows from formulae-as-types but rather from good ol' type safety and enforcement of module boundaries, just as above.
16
17
}
17
18
\p{The [theorems for free](wadler-89) also popularised by [Wadler](wadler), specifically the theorems obtained from the generality of a type signature, are \em{also} \strong{not} a consequence of Curry-Howard, but rather a consequence of the parametricity of the type system.}
···
22
23
\title{Why does this happen?}
23
24
\p{ Many programmers can get swept up in mysticism about Curry-Howard, overstating its consequences. Of these, I think there are two main groups: the \em{mathematically curious} and the \em{mathematical fetishists}. The \em{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 \em{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.}
24
25
}
25
-
\p{Fare more problematic, though, is the culture of \em{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 \em{isomorphism}" because it uses an exclusively mathematical term, "\em{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. }
26
+
\p{Far more problematic, though, is the culture of \em{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 \em{isomorphism}" because it uses an exclusively mathematical term, "\em{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. }
26
27
\p{}
+25
trees/loc-000U.tree
+25
trees/loc-000U.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{The Ascension of the Lord 2025}
6
+
\tag{cmc}
7
+
\date{2025-05-29}
8
+
\author{liamoc}
9
+
\quote{
10
+
Viri Galilæi, quid admirámini aspiciéntes in cælum? Allelúia: quemádmodum vidístis eum ascendéntem in cælum, ita véniet, allelúia, allelúia, allelúia.
11
+
}
12
+
\p{Our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) was the only one in Canberra, it seems, that actually sang at a service \em{on Ascension day}, rather than the subsequent Sunday. We sang Christopher Tye's [The Eternal Gates](https://www.youtube.com/watch?v=hcSou9sCLkA).}
13
+
\quote{
14
+
\poem{
15
+
\line{Th'eternal gates lift up their heads,}
16
+
\line{The doors are open wide;}
17
+
\line{The King of Glory is gone up}
18
+
\line{unto his Father's side.\br}
19
+
\line{And ever on our earthly path}
20
+
\line{A gleam of glory lies;}
21
+
\line{A light still breaks from behind the cloud}
22
+
\line{that veils thee from our eyes.}
23
+
24
+
}
25
+
}