Why Modeling Finds Bugs (Without Model-Checking)

Just the process of writing a model will improve your software designs.

Happy new year everyone! There's gonna be some changes to the newsletter this year, see after the article for details. But first, let's talk formal methods.

I normally sell TLA+ based on the model checker: you give it a design and it tells you if the design has flaws. When other FM experts try to sell TLA+, they focus on the mental benefits of modeling: just the act of writing the model itself helps you find bugs. I avoid this framing because it sounds too much like snake-oil, and because it's the same pitch that all the other correctness disciplines use.

But it's also true! I find a lot of bugs when modeling software and sometimes don't even need to run the model checker. It's a skill you pick up over time. So I got curious about the mechanisms for why it's true. So here's three reasons why the act of modeling itself finds bugs:

Wrong Things Look Wrong

Some software bugs correlate to specific syntax. If you see that syntax, you get suspicious of a bug. Here's one example in code:

for(int i = 0; i <= arr.length; i++) {
  // blah blah blah
}

Most programmers will look at that and immediately suspect an off-by-one error. It could be that this particular code is fine, but writing i <= len quite often leads to a bug. If I gave you some code that did that, you'd look extra hard for an off-by-one.

Similarly, when writing specs, there are certain constructs that immediately make me suspicious about a race condition or liveness bug. For example, if I see

GetLock:
  await lock;
  lock := self;

I'll immediately ask "is there a starvation bug?" In many cases, there won't be, but if there is I'll see it because I'm looking extra hard for one.

Writing > Working Memory

Humans are limited in how much information we can store in our heads at once. If I ask you to add up four 3-digit numbers in your head, you are going to lose track of operations and make mistakes. If you have a pencil and paper, you're going to make fewer mistakes, because you can store intermediate computations and better keep track of your work. Similarly, if I ask you to pick up 10 things from the store, you're more likely to remember them all if I also give you a physical checklist.

In other words, writing lets us keep track of more things. In the case of large systems, "more things" means more interactions between complex components. This is why even writing down specifications in English helps a lot. Formal specification languages just push that further by encoding intricate components more densely, which helps us chunk them up.

Making ambiguity obvious

The worst kind of ambiguity is subtle ambiguity: where everybody hearing the ambiguous thing thinks it's "obvious", but they all disagree on what it "obviously" means. Then people don't realize they need to find agreement because they think they already have agreement. For example, the requirement "there's a limit of 20 requests per minute". There's a couple things that could mean, but it's also not obvious that it could mean different things.

If we try to formally specify it, though, we have to break that ambiguity:

• It could be "for all minutes: messages-sent-between(minute, minute+1) <= 20"
• It could be "for all seconds: messages-sent-between(second, second+60) <= 20"

Writing it formally gives everybody who interprets it differently a chance to notice something's confusing. But it also makes your brain more likely to notice that it secretly resolved some ambiguity, and that maybe you should check it's not supposed to have the other meaning.

But we need the model checker first

These are all important benefits modeling gives you, and they add up to finding bugs without needing the model checker. For many people, these benefits are also more cost-efficient than model checking. Their brain finds 90% of the bugs in 10% of the time, and then the model checker takes 00% of the time to find the remaining 10%.

Even so, I center the model checker in FM. Without it, I don't think many people would ever get "spec-brain". For one, that kind of expertise takes time to train. Most people can't invest time learning something if they only get a payoff 100 hours in. With the model checker, you get payoff much earlier, giving you a reason to keep using FM.

Second, the model checker is a critical part of the training process. Humans learn in feedback loops. You do something, you make mistakes, you get corrected, you try not to make those same mistakes. The longer the feedback loop, the harder it is to learn something. This is one reason (of many) that concurrency is so difficult to reason about. If you have a race condition, you may not find out for a while, and it may take longer to pin the system misbehavior to the race condition.

With a model checker, you find out about the race condition right after writing the spec. The shorter feedback loop means you learn faster. Over time, you don't need to model checker as much, because you've already internalized the feedback it keeps giving you. But you wouldn't have gotten there without the model checker to help you along.

A possible avenue of exploration: what other difficult topics can be made easier with a faster feedback loop? Everybody always talks about how estimation is impossible, but some people can clearly do it well. Maybe there's a way to find errors in estimates quickly and build that skill over time.

Newsletter Logistical Stuff

The main impetus for these changes is that I've left Twitter. While it will assuredly improve my mental well-being, it's not a great change for my professional prospects. I've leaving behind a large audience, a reliable source of client connections, and a medium to share unrefined software thoughts.

So first up, I'm going to be refining a lot more software thoughts. I'm committing to updating the newsletter at least 6x a month, though I really want to try to make it 2x a week. The effort-per-post is going to go down a little bit, but the overall effort is going to go up a lot, so hopefully you'll enjoy the change. This also means that the boundary between newsletter and blog will blur more— some stuff that would otherwise have been newsletters will be upgraded into full blog posts.¹

That takes care of the brain dumping but not the networking. I'm expecting to take a significant income hit this year due from leaving Twitter, due to fewer potential clients seeing my writing. I'm thinking of ways to make that back up and/or create new revenue streams. To be clear, I will not monetize the newsletter, my website, or my guides (learntla/alloydocs/etc). I want to make money to support my teaching, not the other way around.

Anyway, if you like the newsletter, please share it with your friends and coworkers! The more people are reading my stuff, the bigger an audience I have, and the more I can justify my rabbit hole diving as "marketing".

(Also remember that you can always email me at this address! I read all messages sent to me and try my best to respond to them all. I'm also happy to take potential newsletter topics, anonymous or no.)

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.