Proofs, Programs, and Pontification

On HN today, a thread came up discussing the relationship between mathematics and programming. This is always a popular topic, since many programmers enjoy mathematics. However, one particular comment struck me.

A poster made a claim that mathematics and programming are really not all that related to each other. In response, someone wrote “I believe the Curry-Howard correspondence disproves your claim. One can translate between the two and find that they are equivalent.”

I started writing up a brief reply, but things spiraled out of control, and here I am now. I’m sorry in advance.

Why mathematics and programming are not the same

It is both naive and unreasonably ideological to view the Curry-Howard correspondence as justifying a claim that mathematics and programming are equivalent. Let’s start with the naive part.

The “programs are proofs” correspondence links certain proof calculi, such as natural deduction, to certain models of computation, such as the typed lambda calculus. This is, I think, quite an exciting connection to make. But it doesn’t say a whole lot about either mathematics or programming.

I think it is fair to say that most mathematics exists independently, and without much concern for these specific proof calculi. Pythagorean triples were carved into stone tablets by Babylonian scribes thousands of years before Gentzen was even a twinkle in his father’s eye. And despite much well-deserved interest in formal systems as a way of mechanizing the verification of proofs, these tools have never made much headway into mathematics more broadly, which is interested in the human understanding of certain sorts of reproducible mental objects.

With regards to programming, the poster rightfully points out that some languages, like C and Javascript, seem to have not much to do with the Curry-Howard correspondence (since they are not based on the typed lambda calculus…). Language warts aside, it is worth considering whether the extreme success of these languages points to something else: that programming employs a tremendous amount of (and is in fact, dominated by) non-mathematical reasoning.

If we consider a very narrow slice of programming, such as the construction of a function to accomplish a specific task, I grant that this involves mathematical reasoning in the broad sense. Here the programmer must consider invariants and edge cases. More generally, it is of the utmost importance that their code be correct and legible, just as with a mathematical proof. However, one could argue that the careful application of rational thought to reproducible mental objects, which is demonstrated by both the programmer and the mathematician, shouldn’t even be called “mathematical reasoning”, as it shows up in so many other fields. And certainly the interests, objects, and methods of the programmer and mathematician diverge substantially beyond this small point of contact.

Now to consider the bigger picture. Are you a programmer? If so, I would propose to you an experiment: keep a journal for a week, tracking how you spend your time. At the end of the week, work out what percentage of it was spent “doing mathematics” in any form remotely recognizable to, say, a mathematician.

I would imagine that much of your time is spent on other tasks. Organizing and navigating complex systems of code artifacts. Abstraction and API design. Understanding engineering requirements and estimating time commitments. Reading documentation (j/k, reading stackoverflow) and trying to figure out why the build is failing. The list goes on. ¹

Mathematician, Architect, Surgeon, Painter

Many programmers like math. I understand this well, seeing as how I am one of them. For some of them, this interest leads them to functional programming, type theory, and even category theory (or at least, that subset in vogue amongst others who are drawn to functional programming and type theory). It seems to me that this interest starts from a mixture of wanting to improve as software engineers as well as needing something interesting with which to occupy their hobby programming time.

The specific balance between these two motives varies, although the deeper one dives into this stuff the seemingly less interested in software engineering one becomes. And, increasingly, the more that programming begins to look like mathematics. The reason is quite simple: by focusing on a very specific discipline of programming (e.g. dependently typed functional programming) as well as very specific subset of mathematics (e.g. that most closely associated with dependently typed functional programming), the narrower the vision of both fields becomes. To this person, programming is mathematics because they pay little interest or attention to the parts of programming and mathematics that do not fit this formula.

I see some parallels here with the “software architecture” movement. The basic ingredient was the same: ambitious developers, interested in both improving their own abilities as well as finding an outlet for an intellectual drive that wasn’t satisfied in their usual work, sought out metaphors and points of contact in another discipline. In the case of software architects, that involved diving into writings on architecture, urban design, and so forth (e.g. the work of Christopher Alexander). History remembers the worst excesses of this movement: enterprise architecture, design patterns, and so much bad writing. For those of you who are programming Scala by day and learning category theory by night, consider what your legacy will be. ²

What do programming and mathematics have in common?

So what is the relationship between programming and mathematics? I don’t hope to paint a complete picture, but here are some thoughts.

First, there are many points of contact between the two disciplines, across several levels of programming abstraction. This includes lower-level areas such as type theory and digital logic, which provide for basic models of computation. This also includes higher level topics of data structures and algorithms, which in a sense fall under the broad umbrella of discrete mathematics. Even here I find the “Curry-Howard perspective” a bit one-dimensional, since I happen to be a programmer with more of a taste for things other than type theory.

Second, to restate a point I made earlier, there is a common emphasis on “careful application of rational thought to reproducible mental objects”. Both fields involve, more or less, sitting around and thinking through the correctness of something from first principles. However, I would argue that empiricism is also quite important in serious programming, where tests, debugging, and profiling provide the most convenient entry points into understanding program behavior. ³

As a final thought, a few posters in the HN thread poined out that there is, to an extent, a shared sense of aesthetics. Mathematicians do not have much stomach for ugly proofs, and it is common for them to spend a substantial amount of time and energy into polishing things, removing extraneous details, generalizing appropriately, and so on. Many of the best programmers I have met share a similar mentality with respect to the code they produce. ⁴

Footnotes

Site generated by Hakyll