No, "reasoning about code" is not a scam

Late Newsletter next week

Alloy workshop. Still one slot left if people are interested!

No, "reasoning about code" is not a scam

Last week I read “Reasoning about code” is a scam:

More precisely, it’s a thought-terminating cliche. Ironic, as the phrase “reason about” is used as a highfalutin synonym for “think about”. The idea is that there’s nowhere to go from here. I want to do things one way, some random on medium dot com wants me to do things another way, their way makes it easier to reason about the code, therefore that’s the better approach.

I think the piece is wrong, but wrong in interesting ways that are worth discussing. Also I'm always talking about theories of engineering and specification and not so much theories of code, so this is a nice break. Graham makes three arguments:

1. "Easier to reason about" isn't useful information
2. Different people find different things easier, and it's a matter of personal preference
3. Time spent reasoning about code is better spent reasoning about problem domain

At no point, though, does he define what people mean by "reason about the code". "Reasonability" is one of those words that we use ostensively. Nobody has a formal definition of it, just places where we use it because that's where it's used. And that's fine! Many other concepts, like "clever code" and "business logic", are used ostensively. But we can also learn a lot by trying to formalize ostensive concepts. It might not give us accurate or even useful definitions, but it's a place to start thinking.

I will say "reasonability" is a measure of how fast we can accurately answer questions about the code. I make "questions" intentionally broad. This is because most people conventionally say "reasoning" to refer to questions about conformance to specification, which is mostly the same as reasoning about abstract correctness. This is why people generally say that it's easier to reason about pure functions and referential transparency. State mutation makes reasoning about conformance harder.

(Worth also mentioning here: reasoning includes both human and automatic means of answering questions. A type checker can formally answer the question "is this well-typed", and well-typedness is a form of specification. This is why a lot of people say that a good static type system makes code easier to reason about.)

But there are many, many, many more questions we can ask about code! We can ask about its performance characteristics. We can ask about when the source code was last changed and how many lines were changed. We can ask what business problem this code is solving. Some of these may be harder to answer than others, and that changes based on the code. Programs in Haskell, for example, are famous for being easy to reason about correctness and notorious for being hard to reason about space usage. It's not enough to say "this is easy to reason about", we have to say "this is easy to reason about with respect to X."

And knowing that is useful. First of all, it encodes intention. People want to make the code easier to reason about with respect to X because X is important to them. By analyzing the project through an X-reasoning lense, we can get more insight into the system than we could if we just discarded code reasoning as a scam.¹

Second, X isn't just one question. It's a broad category like "extensibility" or "performance" that includes a lot of different questions. Questions that overlap with other categories, like:

• "Will implementing feature Y hurt correctness? If so, what changes do we need to make to maintain our level of correctness?"
• "Will refactor Z introduce a performance regression?"
• "Customers are complaining about bug W. How quickly can we find and fix the problem?"
• "The client wants us to implement feature T. Where would that live in the codebase, and how fast can we implement it?"
• "The business problem has changed from U to V. What do we need to change?"

Notice these are all hybrids between X-problems and business problems. It's important to update your understanding of the problem, but at some point we need to solve it. And the easier it is to reason about X, the easier it is to solve the problem while maintaining (or choosing to sacrifice!) X. Graham says that reasonability is "by necessity accidental complexity". The translation between world and machine is anything but accidental. It's ugly, but it's there.²

That takes care of claims (1) and (3). We're left with (2): even if reasoning about code is good and useful, it's infeasible. Graham argues that people reason about things in different ways, and what's reasonable for me may not be reasonable for you.³

Let’s start with the fact that people don’t think—sorry, reason—about things the same way. If we did, then there’d be little point to things like film review sites, code style guides, or democracy.

Is reasonability really that much like film review? Well, there's lots of different ways to do film review. You could dissect what makes a film work and why. We should do the same with "reasonability", so that it's not just "a thought-terminating cliche". Or you tell prospective audiences whether or not it's worth their time. That usually depends the viewer's preferences, so there's a nice analogy there, too.

Or you could do something like the Rotten Tomatoes, where you just get every viewer's rating and aggregate them. If 99% of people say it's a good movie, then it's a good movie. Similarly, if 99% of developers agree that something "makes code easier to reason about", then that thing makes code easier to reason about. It doesn't matter that 1% of devs don't think that, because 99% of the developers you meet do. So is there some "reasonability" practice that would fit the bill?

Absolutely! Which of these two totally-made up code snippets is easier for you to reason about? Which one makes the bug obvious?

f(...):
  return x*y*z >= w

# ...


can_afford_rec_parcel?(...):
  area = ft_width*ft_length
  return area * COST_PER_SQ_FT >= max_budget

We programmers overwhelmingly agree that decriptive naming makes code easier to reason about.⁴ We break code into functions across multiple files. We use indentation to make subsections of code more evident. We consider lots of globals a code smell. These all affect code reasonability but we don't talk about them because everybody already believes in them.⁵ These might seem like trivial things, but they're all hard-earned knowledge. Practices can go from "thing that only a few people think helps" to "so obvious we consider them trivial." Why couldn't the same happen with other practices? Why can't "use pure functions" become something that's so obvious we don't consider it "reasoning"?

One last thought here, something I strongly agree with Graham on:

More precisely, it’s a thought-terminating cliche.

When we say something "makes code easier to reason about", we shouldn't stop there. We should make clear who finds it easier, what kind of questions we're asking, and how that thing leads to more reasonability. We can't just stop at "this is good", we have to ask why it's good. We have to dissect things. It's in that dissection that we make it, in the end, not a scam.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.