Concerning Quality

The Case for Models

I’ve become a bit model-obsessed as of late. By “model,” I mean a simplified representation of a program. No databases. No HTTP. Just pure logic. What interests me so much about models is that they exemplify software minimalism. We often talk about essential vs. accidental complexity - well, models are the embodiment of the essential. We have an ongoing battle against complexity at the language level, with tons of new languages providing support for immutability, reference sharing control, and other features of modern semantics. But I can’t help but still ask: is it really enough? Is software really getting any simpler?

We all know the opposite is true, and I’d like to make the case for using models to combat complexity.

Models are Simple

First, let me expand on what I mean by “model.” Here’s a model of a bank:

interface Account {
  name: string;
  balance: number;
}

interface Deposit {
  account: string;
  amount: number;

  type: "deposit";
}


interface Transfer {
  srcAccount: string;
  dstAccount: string;
  amount: number;

  type: "transfer";
}

type Transaction = Deposit | Transfer;

class Bank {
  accounts: Account[] = [];
  ledger: Transaction[] = [];

  openAccount(name: string) {
    this.accounts.push({ name, balance: 0 })
  }

  deposit(account: string, amount: number) {
    this.ledger.push({ account, amount, type: "deposit" });
    
    this.findAccount(account)!.balance += amount;
  }

  transfer(srcAccount: string, dstAccount: string, amount: number) {
    this.ledger.push({ srcAccount, dstAccount, amount, type: "transfer" });

    this.findAccount(srcAccount)!.balance -= amount;
    this.findAccount(dstAccount)!.balance += amount;
  }

  findAccount(name: string) {
    return this.accounts.find(account => account.name === name);
  }
}

let bank = new Bank();

bank.openAccount("checking1");
bank.openAccount("checking2");

bank.deposit("checking1", 100);

bank.transfer("checking1", "checking2", 50);

A real bank would have an incredible amount of additional concerns, like security, performance, or resilience. But our model just shows the basic functionality over some basic data structures.

Models are as simple as our problem domain and language of choice will allow. Because of this simplicity, we can look at this code snippet and comprehend it quickly. Of course, complexity will creep in over time as more and more functionality gets added, but even with that added scope, doesn’t a model like this represent the smallest possible description of our desired behavior?

Pretty much all of the benefits of models stem from this minimal simplicity - it’s their most important characteristic. Throughout the years, all of our coworkers, friends, and idols have pleaded with us to focus on simplicity, to the point that it’s become totally memetic. Preaching about simplicity is a great way for us to show that we care, and that we’re going to be the ones to find the antidote to our most recent fall into the tar pit. Heck, I’m certainly not the first person to pitch models as a solution to our problems!

But in many ways, simplicity is more like viewing an electron with a transmission electron microscope - we only see the effects of simplicity on surrounding activities, we can’t really observe it directly. So while I think that simplicity is very important as an ideal, it’s ultimately a trap as a true north star because of our inability to concretely define it. The auxiliary benefits of simple models, though, are more concrete and tangible. Here are some.

Models Cost Less

We know that state spaces grow combinatorially, which makes any form of testing either extremely expensive or depressingly incomplete. This makes the inverse true: models are smaller and have less moving parts than full blown implementations, and this means we can test larger portions of them, quantitatively. With things like bounded model checking, we can also use them to exhaustively test up to a finite bound, which is a really awesome tactic that sits between test and proof.

The Trustworthy Systems group also found that verification effort grows quadratically with code size, meaning the act of verification gets increasingly effortful as the target system grows. I know most of us don’t verify our software, but all of us think about our software, and verification is a fairly good proxy for reasoning - to verify code is to reason about all of its executions against some desired property. So while it is a bit of a stretch, it also feels right: intuitively and anecdotally, applications become increasingly complex to work with as they grow in size.

Both in execution time and in reasoning effort, models are cheaper, and there are lots of awesome tools that exploit this cost benefit. TLA+ is seeing quite a bit of industry adoption, and its toolkit comes with a very powerful model checker. Alloy is similar, with a simpler specification language and a more rigid structure to encourage bounded models which are more amenable to checking. SmallCheck is a particularly cool idea, where you can use property-based testing but with exhaustive inputs up to some depth. There’s also the P langauge which defines itself as “Formal Modeling and Analysis of Distributed (Event-Driven) Systems,” and comes with its own model checking story.

Since each of these are exhaustive in nature, there’s no practical way to use them at the implementation level, and their sweet spot is for checking higher-level designs like models. In Misspecification, I checked an invariant of a model in 26 milliseconds with Alloy. While this is a best-case scenario, it’s an example of the cost savings that models can bring.

Models are Oracles

Have you ever written a bunch of test cases for something where the logic just is the definition of correct behavior? Take a recommendation algorithm. Of course you can write test cases to check the actual outputs of the algorithm, but what happens when you inevitably tweak the logic? How many of those test cases end up changing after the tweak, and what exactly are we testing for in this case? If tests always change along with the implementation, that indicates to me that the code just is the specification.

In my experience, every company has at least one, and often many “secret sauce” calculations like this, but a surprising other example of this arising is in distributed systems (and yes, even a seemingly simple client-server application is a distributed system). While distributed systems are wildly complex, that complexity is often from the simple fact that there are multiple communicating machines involved. Aka, distributed systems are complex because they’re distributed. To a user, though, the overall functionality might be relatively simple, and that sounds like a great case for models! If we have a model of the high level behavior, we can check that the distributed implementation conforms to it.

This is where the notion of a test oracle comes in. It’s obvious, but in order to test something we need to know what the expected value is beforehand. With example-based testing, we are the oracle who knows that answer, and we arrive at that answer by interpreting the requirements of what we’re testing. We encode that knowledge in automanual tests, and we have to use mental energy to decide the expected result of every single test case that we use. If we have a trusted model of those requirements though, we can just check that the implementation agrees with what the model says, in effect only writing a single test.

We have to define what exactly it means for an implementation to “agree with” a model, though, and the most common way of doing this is by showing refinement. Waving some hands a little bit, refinement is a way to show that behaviors in the implementation are also behaviors of the model. If this is the case, then the model and implementation should be equivalent from the user’s perspective since they have equivalent external behavior.

This is the basis of how models can be connected to implementations - by using a model as a test oracle in a test suite. This approach is actually seeing industry application, where AWS now does it to test parts of S3. They build reference models and use them to check properties of their distributed implementations, all in the same language (Rust). I also showed an example of this in Property-Based Testing Against a Model of a Web Application, and as I wrote there, this feels surprisingly good in practice.

The ability to automate tests using a model as an oracle goes away if the model isn’t written in the same langauge as your implementation, but in that case there are lower-tech ways of keeping them in sync. I’ve successfully used models at the start of a feature and then used them to manually generate test cases against the implementation. Then, when a bug or question comes in, I can use the model to first get a bearing on the problem before going through the whole implementation. This is a great, low-cost way to get your feet in the door with using models, and you can do it with something as simple as a spreadsheet.

Models are Documentation

While models are still code, they can be vastly more comprehensible than implementations because of their omissions of all but the most important details. Looking through frontend request caching, backend endpoint definitions, data access layers, database queries, ad nauseum, inevitably clouds the essential behavior of an application. This makes even answering basic questions like “what does the application do in this scenario?” difficult. Again, the size of models is an advantage here, and they can be small enough to actually serve as documentation of a system.

It’s often said that tests are documentation, and while that can be kind of true of good tests, I think it’s missing the point. Tests are examples of behavior, and examples are not specifications - examples are specific, but specifications are general. Take these test cases for the deposit functionality of our bank model, where we’ll extend it to have a maximum deposit amount of $10,000:

describe("depositing less than the max deposit amount", () => {
  let bank = new Bank();

  bank.openAccount("checking1");
  bank.deposit("checking1", 100);

  expect(bank.findAccount("checking1")!.balance).to.eq(100);
});

describe("depositing more than the max deposit amount", () => {
  let bank = new Bank();

  bank.openAccount("checking1");
  try {
    bank.deposit("checking1", 10001);
  } catch(e) {
    expect(bank.findAccount("checking1")!.balance).to.eq(0);
    expect(bank.error.message).to.eq("Attempted to deposit more than the maximum deposit amount")
  }
});

These are two specific scenarios of depositing money. Compare that to the definition of the deposit method in the model:

deposit(account: string, amount: number) {
  if (amount > MAX_DEPOSIT_AMOUNT) {
    throw new Error("Attempted to deposit more than the maximum deposit amount")
  }

  this.ledger.push({ account, amount, type: "deposit" });
  
  this.findAccount(account)!.balance += amount;
}

Because the model code is written at a higher abstraction level, it’s pretty much a direct transcription of the specification of our desired behavior. In English, this code reads as:

“When an account is deposited into, an error is returned if the max deposit amount is exceeded. If it’s less than the max deposit amount, a deposit ledger entry is created and the account balance is incremented by the deposit amount.”

For me, the model version is better documentation than the examples, and it’s only possible because implementation-level concerns aren’t present. I’m not commenting on example-based TDD being beneficial for figuring out the best interfaces for modules, or any other benefits of examples, but I don’t think examples end up being the greatest form of documentation. The issue is that there’s an impedance mismatch between a specification statement and the examples that are necessary to exemplify it. Here, we chose 2 examples to test a single if statement. Obviously, for more complicated logic there will be more branches in the code, and that will translate to more examples to cover the branches.

I find that a concise and accurate description of desired logic in the form of a model-based specification is more clear than a set of 10 test cases. This also highlights that, in models, we can write them to be communicative, and not necessarily worry about efficiency since that’s an implementation-level concern. The simple act of modeling allows us to write with more clarity. Information sharing becomes a dominating factor in the efficiency of a team as it grows, so this communicativity is extremely important, and something I find lacking in most projects. Models provide an efficient way to share the most important information about a software product: what exactly the product does.

Models are Fun

Do you remember when programming was fun? When you were first learning and felt like you could build anything? I remember that feeling, but only distantly, because it’s pretty rare that I feel it recently. Obviously enjoyment is multidimensional, but I think a big part of it boils down to economy of motion. Programming is fun when the changes you want to make are easy and fast, and you don’t have to spend days messing with your tools and codebase to get there. The distance between the idea in your mind and a tangible application that a user can interact with is clearly inversely proportional to how enjoyable it is to build the application.

Models are fun! Focusing on pure logic and solving a problem at the user level is highly enjoyable, and it reminds me of what I love about software. I like building interactive applications that make people’s live’s better. The tests that I write on a daily basis don’t seem to be related to that goal at all, no matter what design pattern I’ve tried at the implementation level. The only way I’ve found to have good economy of motion is to drastically reduce the raw size of code that I work with, and have a codebase that has a fast feedback loop. Because models are pure-logical in nature, they achieve that.

Contrast this with an all-too-common experience of programmers becoming jaded over time and eventually leaving a project just to experience the joy of greenfield again. This often happens because the project becomes way too hard to modify and too time-consuming to maintain. Models are easier to change or extend, so using them in a development workflow can help keep a project engaging for longer.


To sum it up: models are fun, simple, and cheap artifacts that can even act as your source of truth in tests. We should use them more!

The Dark Side of Models

I don’t mean to suggest that models are a silver bullet. Models have a number of tradeoffs. The first major one is similar and related to the verification gap - what the heck do you do with a model after you’ve built it? How do you connect it to an actual implementation? If you don’t, then it’s only a matter of time before they drift away from each other, and when you’re in a time crunch you’ll end up tossing the model every time. As mentioned, there are concepts like refinement for checking model conformance, but those require constraints like having an executable model. I don’t want to underplay this - this is a huge problem, but the verification gap post does outline some potential solutions. Long story short, some part of your process has to continuously use and modify the model, or it will simply atrophy.

There are also cases where the delta between the model and the implementation isn’t that large, so you don’t get a ton of extra benefit over just using the ipmlementation. If your model and implementation are just duplicates of each other, the model is not simpler, and therefore all of the auxilliary benefits of them won’t be there. There’s no value prop here.

Controlling the bounds of models is also a delicate art. Model checking is great when the state space of a model is small, but the sate space of even simple models can blow up past the point of being easily checkable. This art can be learned, but it’s not free.

Models are also just plain different. An implementation is the only required artifact that we need for a functional application, and we already have test suites as a de facto addition for continuously checking the quality of implementations. It’s not clear where models fit into this setup - is it possible for them to replace test suites entirely, or should they simply augment them? If they augment them, that’s just another thing to learn and maintain. A good model-based workflow is definitely not something that you can pick up off the shelf, since it’s not very common. Innovation budgets are only so high, and incorporating models at this point in time will require innovation.

Models also don’t get rid of implementation complexity. If you want to debug a performance issue, that has to be done at the implementation level. Same goes for monitoring, I would never suggest that the presence of a model eliminates the need for monitoring the real production system.

There’s also a sub-community built around “Model-Driven Architecture” that apparently has had some divisive experiences, which is important to acknowledge because it’s not like we’ve never tried model-driven workflows before. From what I gather, this seems to be based on UML as the modeling language though, which is definitely different from what I’ve been thinking about in source-code based models. It’s entirely possible that if we become open-minded to models we’re just going to be repeating history, but if anyone has any concrete case studies to share here I’d love to hear them because I don’t know of any.

Of course, all of these problems also present interesting research ideas and problems to solve.


One Last Plea

Again, I’m writing about models because I have a deep desire to keep software minimal. While I don’t think it’s wrong to simply buckle up and deal with the complexity and raw magnitude of implementations as many of us do, that’s just not the path that I find appealing intuitively. I want to at least try and propose an alternative, and right now that looks like adopting modeling and model-based workflows for the reasons presented here. Models are small and minimal, which makes modeling stand out as a compelling technique with simplicity at its center. Problems that we wouldn’t even dream about trying to solve become manageable with models, like exhaustive model checking of bounded state spaces. The gap between model and implementation is real, but we have options for connecting them.

As an industry, we’ve had our hands full for quite some time pushing forward what’s possible. We’ve built new CPU architectures, machine interconnections, programming languages, operating systems, GUI frameworks, and countless other tools to make a truly incredible modern toolkit for building software - and most importantly, we can build novel software that wasn’t possible even just a few decades ago. With no disrespect to what we’ve built to get here, there’s a price to this progress though, and the load on the average programmer’s mind on a daily basis is at an all-time high.

This makes me think of the quote from Alan Perlis, the winner of the first Turing Award:

Simplicity does not precede complexity, but follows it.

I am interested in a simplification of our current workflows, shifting from what’s possible to what’s manageable. We have the vantage point of being around after the creation of tons of technologies, but we have no way of wrangling everything that goes into a software product. Models are natural wranglers, by describing parameters and boundaries of logical behavior in the simplest possible way. I’m hopeful that they can be used to transition us away from complexity.