TLA+ for startups (part 1)
Why formal specifications are not a completely insane idea for startups and small teams
This is the start of my personal and professional journey into the formal specification language TLA+. Before we dive into the details, I should probably begin by explaining my motivation for creating this series of articles.
Startup life: right thing, right time, done right
In my professional life, I build and run software development teams that create business systems using some of the latest technologies and methodologies. The systems we build are complex, but not Apollo programme or nuclear power plant complex. Thousands of lives may not depend on us writing robust, reliable and correct code; but if we write brittle, unreliable and faulty code, the company’s reputation will suffer, our clients’ reputation will suffer, and we will lose money.
The quality of the systems we build could make the difference between us winning in our chosen business domain and failing, badly. As I work in startups, marginal losses from poorly thought-out business strategies, poor tactical choices, or badly written code can take you very quickly indeed to the end of the road.
So there is a very real incentive in my world to create software systems that are right. Now there’s a funny word. That could mean a lot of different things to a lot of people. At one end of the spectrum, I could spend millions (somebody else’s millions, that is) creating a software solution that fully solves every significant problem in my company’s chosen business domain… only to find that there is no market appetite for 90% of what we’ve built, and as a result we will never come close to recovering the cost of the build.
Or I could create a super-lean, MVP solution to a very specific problem, promote it aggressively to gain traction in the market quickly… only to find that the shortcuts we made in getting there quickly come home to roost, while I watch a competitor coolly and calmly launch their product three months later that fixes all the shortcomings in our solution.
In short, the reason why startup life is a lot harder than it looks is that you generally have one shot at getting it right. And that means you have to build the right thing, and you have to build that thing right. Oh, and you have to do all that at exactly the right time.
Pragmatism is King
Common sense would have it that, to hit the sweetspot in the middle of the Venn diagram above, the startup tech lead has to be supremely pragmatic. If you think you can succeed in the startup world by overburdening your team with detailed processes, design frameworks and formal practices, you will have a very rude awakening. You have to be lean and mean; fast and furious. You have to be the gazelle to the corporate dinosaur; the speedboat to the corporate oil tanker.
Conventional wisdom would tell you that formal specification languages are wholly unsuited to startup life
If common sense tells you that you have to be fast, lean and supremely pragmatic, then conventional wisdom would also tell you that formal specification languages are wholly unsuited to startup life. It would probably be safe to assume that, on a continuum of the amount of effort invested in the design stage of software, most people would place formal specification languages way over on the right. Startups should be picking from somewhere near the left, and ought to be leaving formal specification languages to the superbrains designing missile targeting systems for fighter jets.
But is that true?
Luck be a lady tonight
Thinking about the Venn diagram and the continuum diagram together, we have a contradiction. On the one hand, we’ve identified that startups typically have one shot at getting it right (right thing, right time, done right). But on the other hand, conventional wisdom tells us that we need to do it with almost the lowest possible amount of investment in the design stage (also known as the thinking stage).
In other words, if we are to succeed, we’re going to need to get very, very lucky.
So what are you, our long-suffering startup tech lead, to do? Should you gradually and gently be moving rightwards on the continuum of pain? Maybe at first asking your team to sketch out their designs on a whiteboard before writing code? Then when that no longer feels fit for purpose, employ a BA to start writing something that at least looks a bit more thought-out? And then maybe 12 months later give one of your best developers an “architect” title and ask them to start drawing proper diagrams? You vaguely remember that formal specification module you did for a semester on your CS degree all those years ago, and you tell yourself that maybe you’ll find a use for it one day… but of course you’re not building software for controlling the coolers in nuclear reactors so… y’know.
While you are pondering your journey along the continuum of formal design, there’s a pretty decent chance that you have been distracted by some pretty major firefights in v1 of your solution; the lead developer you would’ve given the architect title didn’t turn up to work three weeks ago last Monday and you haven’t seen her since; the client you were counting on winning won’t sign the contract because they kept getting timeouts on your demo environment.
Perhaps all this could have been avoided if you had done a bit more design upfront, but hindsight is a wonderful thing, and frankly you didn’t have the time.
Before you know it, your startup dream is lying in tatters.
As I say, you’re going to need a lot of luck.
Thinking is underrated
That was a lot of preamble to bring me to the real point of this first article in the series ‘TLA+ for startups’.
I guess the title gives it away. I would like you to throw out your preconceptions about formal specification languages. Despite what you might think, they’re not just reserved for arcane computer science problems or hyper-critical systems.
Most importantly of all, TLA+ helps you THINK about the problem you are trying to solve
Although it builds on a rich history of formal specification theory and practice, TLA+ has been designed for solving real-world computing problems. But most importantly of all, TLA+ helps you THINK about the problem you are trying to solve.
It can be applied to a wide range of computing problems from simple algorithms through to large scale distributed architecture designs. It does not require years of training or a PhD to get started, just a grounding in some relatively straightforward mathematical concepts.
I believe that TLA+ enables software engineers and systems analysts, for the first time, to practically and formally reason about the code they are going to write before they write it.
The formally part I will leave to a later article, or indeed point you to some of the links sprinkled throughout this or later articles. Other people far smarter than me can explain why formal reasoning about systems using the universal language of mathematics is an incredibly powerful and useful thing to do.
The very act of attempting to describe the properties of some code you are planning to write is often enough to spark a new way of thinking about it
But practically, because despite what you might assume, it is definitely possible to get started with TLA+ quickly and start leveraging value from it right away. The very act of attempting to describe the properties of some code you are planning to write is often enough to spark a new way of thinking about it; to reveal a nuanced insight into the problem that you are trying to address; to tease out a logical flaw in your assumptions.
I often advise engineers on my teams to either sketch a design or write down in plain English the main tasks that they will need to complete before writing any code. The reason I suggest this is that doing so forces your brain to conceptualise the problem in a subtly different way, and the result will often be quite enlightening.
***In these two similar lectures (here and here), Leslie Lamport, inventor of TLA+, explains the importance of thinking above the code, and how TLA+ helps you to do that.***
Eating the elephant
You can start by using TLA+ or its alter-ego PlusCal to describe a small part of your system. Perhaps there is a short but non-trivial algorithm or logical flow in your system that you are pretty sure you can just go ahead and code, but you want to just validate your thinking on it before you do. Once you’ve got your head around the basic structures and semantics of TLA+, this would be a perfect candidate to get started on.
Importantly, you do not need to eat the whole elephant in one go. If your first use case for employing TLA+ in your design process is describing a high throughput, highly parallelised, distributed software architecture, you’re going to get your fingers burned. Or should I say you’re going to choke on a tusk.
Recalibrate your thinking
I would urge you to recalibrate your thinking about the role that formal specification languages can play in your design process. I would argue that TLA+ makes it possible for you to introduce some formality into your design process much, much earlier than before, and indeed I would recommend introducing it BEFORE considering other structured design practices such as UML.
I’m not arguing against using these practices — they can be extremely useful. I’m arguing for easing into the habit of formally describing the intended behaviours of your system so early on that it becomes second nature. It is something that you and your engineers and analysts can practically do before you need to consider more heavyweight, structured processes that will inevitably come as your company grows.
This series of articles attempts to make the case that TLA+ and startups are actually very happy bedfellows
In short, this series of articles attempts to make the case that TLA+ and startups are actually very happy bedfellows. It gives you a toolset by which you can improve your thinking and reduce your chances of making those critical design mistakes early on, with surprisingly low upfront investment. For the specific challenges that startups face, as discussed at the top of this article, that little bit of extra thinking, done in the right way, could be the difference between glory and ignominy.
*** In this video, Hillel Wayne (author of Practical TLA+ and the LearnTLA+ website), does a very good job of demystifying the core concepts of TLA+ and demonstrating how it can be used practically for smaller problem domains.***
What to expect
Now I’ve made the case for tech startups considering adding TLA+ into their armoury, in subsequent articles I will get practical. I’m going to build up an example of a real-world system that everyone can relate to, one that is simple to understand but a little more difficult to reason about. I’ll use TLA+ to help me do so.
I am definitely not an expert on TLA+, and might never be. Rather than just talking the talk, I am going to attempt to walk the walk of proving that TLA+ can be usefully employed at an early stage of system design thinking, with an appropriate amount of time investment for a small business, and can grow with you as your system matures.
I may fail in my quest. But hey, I work in startups, so I’m not scared of that as long as I’ve given it my best shot!
A few important links
Leslie Lamport’s official video course
Leslie Lamport’s TLA+ Hyperbook
Hillel Wayne’s Learn TLA+ website
The TLA+ Google Groups community
Leslie Lamport’s seminal work, Specifying Systems, also available in PDF format here
I’ll introduce more links as we go along, but these are, in my opinion, the building blocks upon which you should begin your TLA+ journey. Also buy Hillel Wayne’s excellent book.
