Infinite Negative Utility

This post is a bit more opinion-heavy than my usual fare here, but I wanted to lay out my position on this pretty clearly so I can point to it in the future.

I recently saw a comment on Twitter which irked me a bit. I'm not going to link to the original—I certainly don't want to start the kind of argument Twitter is infamous for!—but the comment went:

From a Curry-Howard perspective, “I like programming but I don't like maths.” means “I like programming but I don't like programming.”

I objected to this on Twitter as well, but it's hard to be nuanced or insightful in 140 (or even 280) characters, so I'm writing this slightly longer, hopefully clearer explanation of what it is that bothers me about this sentiment.

My first objection is that this sentiment draws an analogy that is materially and practically incorrect: when someone says, “I like programming,” it is a safe assumption that they mean, “I like sitting down at a computer and using various tools to describe software that I can then run.” On the other hand, when someone says, “I don't like maths,” it is a safe assumption that they mean, “I don't like performing operations in formal systems in my head or on paper in order to solve problems.” These two tasks are, in material and concrete terms, not the same: the way you set about them is often different, the artifacts you produce and the goals you have are often different, and the problems that arise in the course of performing them are often different! (I rarely have to debug segfaults when I do pen-and-paper mathematics, for example.)

You might object that programming and math do have much in common: in order to write a good program, you have to simulate a formal system in your head before you run your program just as in mathematics, and you also you can perform mathematical tasks using a computer-aided sytem (e.g. with an interactive theorem prover like Coq or Lean.) And there are some common goals, common artifacts, and common problems between the two. All that is true: programming and math have a common structure, and there are strong overlapping areas of practice, and I would argue that we should make the practices of both computing and mathematics more like each other! But for many people who do math or programming or both, the two activities are decidedly not identical.

Consequently, a reasonable interpretation of the sentence, “I like programming but I don't like maths,” might be, “I like making a computer do things but I don't like simulating a formal system on paper,” and indeed, if someone said this to me sans context, this is probably what I'd understand it to mean!

My second objection is that it's a somewhat broad (although not at all unusual) overstatement of what the Curry-Howard Isomorphism actually is. The Curry-Howard isomorphism is generally stated as, “Proofs are programs and programs are proofs.” Already, we can see a problem: the comment in question didn't say 'proofs', it said 'maths'. There are many things that a person might refer to as 'maths' that are not just proof-writing.

And even that short statement of Curry-Howard is a bit reductive: the Curry-Howard isomorphism is actually an isomorphism between proof calculi like natural deduction or sequent calculus, and static type systems for models of computation like the simply typed lambda calculus. Many programming languages—especially statically typed functional languages like Haskell and OCaml, but by no means only them—have type systems that correspond to reasonable proof systems, but many other programming languages used in practice have static type systems that correspond to unsound or nonsensical proof systems, and many other programming languages used in practice are dynamically typed and therefore have little if any meaning when viewed through the lens of Curry-Howard!

So Curry-Howard is not really about all programming, nor is it about all math. An accurate statement might be, “All programs in typed languages correspond to proofs in a formal proof system,” but that might be excessively pedantic, and it's rather a lot of characters to tweet. “All programs are proofs,” is reductive, but probably fine in context. “All programming is math,” is a clear step beyond what the Curry-Howard Isomorphism actually means.

Now, to be clear, the Curry-Howard isomorphism is an incredibly powerful idea, and I genuinely think that working programmers should be familiar with it. But assembly-language programming is also programming, after all, and it's not isomorphic to proof-writing in the same way that Haskell programming is.

My third and biggest objection to this statement is much, much simpler: it's divisive and, well, smug. While I nitpicked the phrasing above for being over-broad and reductive, I did carefully mention that there's still truth to it: someone steeped in the kinds of programming and mathematics where Curry-Howard is commonly cited likely wouldn't bat an eye at the quote! Programming (of a certain kind) and mathematics (of a certain kind) are deeply intertwined to the point of being slightly different views on the same underlying concepts and activity—and to the extent that they're not, I'm sure the sure the originator of the quote would agree with me that we should endeavor to bring them closer together by both tooling and practice.

But it's important to note that not everyone does this kind of programming or this kind of math. For a person whose exposure to mathematics is calculus and statistics, and whose exposure to programming is Python and R—a likely scenario for many people who do scientific computing!—the sentence above comes across at best as obscurantist and pedantic, at worst as nonsensical. This is true even for several working programmers and mathematicians to whom I mentioned this quote. Its phrasing is clearly intended to wow people, to evince a deep and perhaps surprising truth about the practices of math and programming: “Programming and math are exactly the same thing, have I blown your mind yet?” This quote is also radically non-applicable to the experience that many people have had of mathematics and of programming. When such a person reads the statement in question, it comes across as being a self-satisfied kind of ivory-tower sentiment.

Which—not at all coincidentally!—is exactly the impression that many working programmers have of functional programmers.

The person who wrote the original comment apparently saw my criticism—at least, he identified that criticism existed, and I can only assume that he was referring to mine—and his rebuttal was this:

What good does it do you for programming not to be a mathematical activity?

This comment is a pretty radical misreading of what I had said: I was specifically criticizing the rhetoric, not the content, and my comment had even identified this kind of statement as coming from “...people I in general basically agree with.” But even so, the content of this restatement is not actually the same as the content of his earlier statement: the first one glibly identified programming as identical to mathematics while explicitly minimizing any difference between them, while the second comment claims programming is a mathematical activity, a much weaker, less contentious, and less divisive statement.

Is programming a mathematical activity? Very often, yes! And I would contend that our work as programmers should be to make programming even more of a mathematical activity than it is already. We should build proof tools around code and simultaneously make code more amenable to proving. We should educate programmers about the kinds of mathematics that can make their day-to-day job of programming easier and more powerful. We should elucidate the existing mathematical structure they might not realize is already present in what they're doing. And we should build new mathematical abstractions that can benefit both programmers and mathematicians in new and powerful ways.

Right now, many programmers don't think of themselves as mathematicians. In order to bridge this divide, it's important to reach out and talk to these groups in the language that they understand: exposing the mathematical structure of programming and illustrating through example and practice the power of understanding programming as a mathematical activity.

But if we articulate our position as, “Math and programming are identical, have I blown your mind yet?” we don't come across as people trying to push for a better world, who are trying to share tools and knowledge to make both mathematics and programming better. We come across as preaching sectarians, and we unfortunately become yet another data point for the “functional programmers are smug and out-of-touch” pile.