The Puzzle of Programming

Lessons from the Curry-Howard Correspondence

A Quick Update

I have put the first chapter of Runnable Specifications online! I had some trouble with the HTML export. There are some issues I’m still trying to fix. However, it’s 99% there.

The chapter is by no means complete. I would like to add a lot of exercises. But it has passed the point where it is worth people’s time to read it. And it’s content-complete. It says everything I want to say in that chapter.

I would love comments and suggestions. Specifically, I’m looking for the following:

• What parts did you find insightful?

• What surprised you?

• What was slow and boring?

• What was confusing?

• What is missing?

Thanks! Just reply to this email, and I’ll read it.

You can read the chapter here.

And now, the essay …

I’ve been itching to learn a new language for a long time. I considered Rust, but I couldn't get too excited any time I looked at it. Elixir looks cool, too, because I think there’s a lot to learn in the Erlang ecosystem. But for some reason, it never stuck.

Over the weekend, I started learning Agda. Agda is a dependently typed language. Think of it like Haskell with an even more logic-oriented type system. I’ve been working through a booklet called Programming and Proving in Agda.

Agda makes the Curry-Howard Correspondence so palpable. As I work through the exercises, I can feel that logic and code are deeply connected. I would feel this in other functional languages occasionally, but it happened repeatedly while I was exploring Agda, almost in every exercise I did. Writing code felt like a puzzle in a good way.

It happens in Clojure, too. Sometimes, while writing some code, I know the types of the values I’ve got in the local variables: a sequence and a function. Really, the only thing that can make sense is to call map with those two arguments. Likewise, if I have a map of keywords to numbers and a keyword, and I need a number, it’s obvious to get the value from the map at that keyword.

This view is directly opposite a step-by-step, almost algorithmic approach to the problem, where I’m trying to come up with what steps I need to write to accomplish a goal. Instead, it feels much more like a logic problem where you use a combination of deduction and process of elimination.

But then I thought of the quote by Rich Hickey regarding puzzles that I mentioned a few issues ago:

And these type systems they're quite fun, because from an endorphin standpoint solving puzzles and solving problems is the same, it gives you the same rush. Puzzle solving is really cool. But that's not what it should be about. […] Solve problems, not puzzles.

But what if you turn your real problem into a puzzle and then solve it? You make your work fun, and you use a different part of your brain that might be better for that particular problem. That’s what it feels like in Agda. And what if you’re doing it for fun anyway, not for work?

Now, I know a lot of people will wonder whether I’m joining the other side—the pro-type side. Listen, there are no sides. It’s a dumb debate. I like types, and I like untyped languages. However, I prefer Clojure for many reasons, including that it is untyped. So why am I exploring Agda?

Conal Elliott (who recently switched from Haskell to Agda) said something on a podcast that got me thinking. He talked about how it does take longer to program something in Agda because of the burden of proof required to write type-correct code, but you’re creating something whose value will last forever because it is a mathematical proof. That appeals to me for certain projects. But at the same time, there are often practical problems where the solution does not need to have lasting value. For those things, I prefer Clojure.

Agda is teaching me things. It is awakening my love for logic and mathematics and their relationship to meaning and ideas. Learning it is hard, but anything worthwhile is. It’s scary because there’s so much to learn to get anything done in it. But the process of learning is rewarding, so I’m going with it. I anticipate that all of my code, regardless of language, will get better because of it.