April 30, 2021

Can Formal Methods Succeed where UML Failed?

Last Tuesday's piece Why UML "Really" Died went viral. I'm glad that people enjoyed it, and I also was happy to use all that fallow research, but something's been bothering me. People didn't switch from UML to something else; they walked away from the mindset entirely. UML wasn't fulfilling a meaningful use case for programmers, so when it didn't work they didn't look for an alternative. The last five years of my life have been dominated by an "alternative": formal methods. I teach people how to write blueprints of a system in TLA+ or Alloy.¹ Why should I believe that formal methods will succeed where UML failed?³

Throw out all of the circumstantial advantages, like "it has a text format" and "it's significantly less complicated", and think about the essential value-add. The "point" of UML was blueprinting. People could design their software projects before implementing them. That's the point of formal methods too. The fact that people didn't look for UML alternatives should worry me. It could mean that modeling isn't useful to software engineers, so FM wouldn't be either. That's too terrifying to think about, so instead I'm settling on a more optimistic take: modeling can be useful, but UML didn't make it worthwhile. That's, at least, more tractable. We can ask how formal methods makes things more useful.

What did using UML actually get you? The dream was roundtrip code sync between UML and code for model-driven development, but that dream was never realized. Through its entire life the value of UML has been in having the UML diagram. It's supposed to help you communicate precisely with your team and use as a reference for writing the actual code. These weren't enough to make it useful, though– even the people who defend UML use only a handful of the diagrams, and as a sketching notation, not a blueprinting notation. And given nothing replaced it, having a design wasn't deemed useful in principle.

I guess that makes sense? A design is only helpful if it saves significantly more time or resources (in performance or release bugfix time or the like) than not having a design. The calculus gets even worse if we also factor in the opportunity cost of learning the design technique. Spending an hour of UML to save two hours of implementation isn't worth it if it took you a month to learn enough UML! Maybe saving an hour per project adds up over years on the job, but that assumes the developer will keep using UML. The design technique has to provide tangible benefits right out the gate or people won't commit to it.

That's if formal blueprinting is useful. People say it is, but people say lots of things. Maybe design is good, but designing in a formal notation isn't sufficiently better than drawing lines and boxes on a napkin. Why invest the time to learn a formal technique? Any response I have to that must make FM worthwhile without also making UML worthwhile, because then it's too weak of a reason.

Here's what I've come to: imagine we create three designs of a system, one using something like Alloy, one using UML, and one as an informal sketch. After we implement the designs, we discover a bug in the wild: all three codebases break an important invariant. There are basically two possibilities:²

1. The design doesn't uphold the invariant.
2. The design upholds the invariant, but we implemented it wrong.

For the informal sketch, we can figure out whether we have (1) or (2) through investigative techniques: thinking about the design really hard, debugging sessions, making and testing predictions, etc. With the UML model, these are potentially easier, and you can potentially think about the problem more clearly. But it doesn't add anything else to our toolbox, at least not with current tools. You're still doing the same things, except maybe faster.

To be more useful than the UML, then, Alloy needs to provide a new, more useful way of distinguishing the two possibilities. If we can automatically identify designs that don't uphold properties, we can rule them out before starting. This has the potential to offer a lot more obvious-value than UML had. Instead of helping you find a good design through some wibbly-wobbly "it helps you think better", it helps you find a good design by telling you if your design is bad.

And there is a way FM can do that: model checking.⁴ The model checker takes a specification and a set of properties and tells you if the spec breaks those properties. Passing the checker doesn't always mean the design is good, but failing the checker almost-definitely means the design is bad. And then you don't implement it! You implement something else.

That's the benefit that originally drew me to formal methods, and it's the benefit that makes FM actually worthwhile. Being able to automatically catch design mistakes before you start implementing saves a huge amount of time in the long run. For some reason, a lot of experts (including me!) can lose sight of that benefit and think the main value of FM is in the "think better" bits. But UML also helped people think better, and that wasn't enough to make it work. Not that people don't want to "think better", but they're skeptical of whether tools can actually deliver that claim. Whereas "this finds bugs for you" is tangible. You can run it for yourself and read the error trace.

That makes me a lot more confident about the long-term sustainability of FM tooling. Then again, I can just be deluding myself. Of course I want FM to succeed. My salary depends on it.

---

Unrelated Thing

This is the first time I distinguished "obvious-value" from "value". I think I like that distinction. Sometimes things have value in ways we don't realize. Since we don't notice the value, we don't factor it into our decisions. Something can be incredibly helpful to us, but we don't know it is, so we abandon it.

Similarly: a couple years back I wrote a thing on the science of software quality. In it I argued that things like sleep and stress affected code quality more than things like language choice or specific discipline used. My favorite bit:

Work-life balance and wellness impact us in a subtler way than technical practices do. It’s easy to point to a bug and say, “This couldn’t have happened in Rust.” It’s a lot harder to point to a bug and say, “This wouldn’t have happened if the programmer wasn’t stressed out and sleep-deprived.” There’s no feedback loop that pushes developers away from too much stress and too little sleep.

Same idea, really.

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.