my forest
update cc and screed
+90
+6
trees/dt/dt-macros.tree
+6
trees/dt/dt-macros.tree
···
16
16
\title{\tile}
17
17
\body
18
18
}}}
19
+
\def\thesisblock[body]{\scope{
20
+
\put\transclude/toc{false}
21
+
\put\transclude/numbered{false}
22
+
\subtree{\taxon{Thesis}
23
+
\body
24
+
}}}
19
25
\def\upshotblock[body]{\scope{
20
26
\put\transclude/toc{false}
21
27
\put\transclude/numbered{false}
+30
trees/loc-000R.tree
+30
trees/loc-000R.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{5th Sunday after Easter 2025}
6
+
\tag{cmc}
7
+
\date{2025-05-25}
8
+
\author{liamoc}
9
+
\quote{
10
+
Vocem iucunditátis annuntiáte, et audiátur, allelúia: nuntiáte usque ad extrémum terræ: liberávit Dóminus pópulum suum, allelúia, allelúia.
11
+
}
12
+
\p{This week our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) were again without a director, so I conducted as we sang Théodore Dubois' setting of the Good Friday Antiphon [Adorámus te, Christe](https://www.youtube.com/watch?v=n4pKqXGo7Ak).}
13
+
\quote{
14
+
\table{
15
+
\tr{
16
+
\td{Adorámus te, Christe,}
17
+
\td{We adore you, O Christ,}
18
+
}\tr{
19
+
\td{et benedícimus tibi,}
20
+
\td{and we bless you,}
21
+
}\tr{
22
+
\td{quia per sanctam crucem tuam}
23
+
\td{because by your holy cross}
24
+
}\tr{
25
+
\td{redemísti mundum.}
26
+
\td{you have redeemed the world.}
27
+
}
28
+
}
29
+
}
30
+
\p{I also attended Evensong again at [St. Paul's Manuka](https://www.stpaulsmanuka.org.au/). Unlike last week, the proper choir was in this time, and they used the 1662 Book of Common Prayer rather than the much inferior Common Worship. The preces and responses were from Philip Moore's \em{Third Service} and the anthem was Samuel Wesley's [Blessed be the God and Father](https://www.youtube.com/watch?v=389leQkiGgk). I've definitely sung this at some point, but I don't recall if it was at Ainslie or at [St. Michael and All Saints, Edinburgh](https://smas.church) (I think the latter). The St. Paul's Choir has some very proficient sopranos, but my biased opinion says that our group at Ainslie sings more musically and in better ensemble. }
+26
trees/loc-000S.tree
+26
trees/loc-000S.tree
···
1
+
\import{dt-macros}
2
+
\date{2025-05-25T13:36:39Z}
3
+
\title{Against Curry-Howard Mysticism}
4
+
\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
+
\thesisblock{
7
+
\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
+
\p{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!).}
10
+
\p{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 \em{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. }
11
+
\subtree{
12
+
\title{But I get theorems from the types!}
13
+
\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
+
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
+
\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.}
18
+
\p{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 \strong{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](dt-001Y)) — the meanings of types, not their logical analogues.
19
+
}
20
+
}
21
+
\subtree{
22
+
\title{Why does this happen?}
23
+
\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
+
\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{}
+1
trees/loc-000T.tree
+1
trees/loc-000T.tree
···
1
+
\date{2025-05-25T14:19:24Z}
+3
trees/people/wahoward.tree
+3
trees/people/wahoward.tree
+6
trees/places/fpca89.tree
+6
trees/places/fpca89.tree
+6
trees/refs/howard-80.tree
+6
trees/refs/howard-80.tree
+5
trees/refs/wadler-14.tree
+5
trees/refs/wadler-14.tree