It seems like this book would have a pretty limited audience since, looking at Wikipedia at least, TLA+ is primary used at big cloud providers who are writing low-level distributed systems stuff.
Can any mortals who've used TLA+ discuss their motivation for using it and the impact it had on their project? I imagine you'd have had to work in a technology-driven environment to be able to justify it to management since formal verification isn't even in the vocabulary of most ordinary development shops.
Hey, author here. While right now TLA+ is most popular with cloud and infrastructure companies, that's more because it already has a reputation there than anything. As u/bmays mentioned, at my previous job we were using it to verify device setup, vendor integrations, and business logic. We only had ten engineers in the company, but our estimates it usually cut development time by a quarter and almost entirely eliminated post-release fires. I've also heard stories from a lot of people who've learned TLA+ from my material and, while I can't give identifying details, I can provide some high-level descriptions of what they did with it:
* A few different groups verified business ETLs with it, finding corner cases which would lose or corrupt data. Similarly, I a lot of use for deployment procedures.
* A lot of people are using it for testing optimizations: write a TLA+ spec of your system, write a spec of the optimizations, and check that they have the same behavior.
* Finding bugs in microservices. I get a _ton_ of emails about this.
* Lots of specific domain problems: trading algorithms, robotics, etc.
The main benefit of TLA+ (and formal specification in general) is that it gives you a way of both writing a precise design of your system and checking the design itself for bugs. That's something so rare in mainstream programming that many people don't even know it's possible. That's why I want to make this stuff more accessible.
Yes, very helpful, thank you! I'd like to see methods like this go mainstream. The prevalent view these days seems to be that software construction begins and ends with unit tests... I don't know how Uncle Bob and his ilk managed to drown out all of the other approaches to construction, but it's always bothered me that even lightweight approaches to verification (like Design by Contract) haven't gotten the same traction. (I suspect it's because formal verification involves more requirements gathering and design work up front, but a lot of teams short-change that because "we're doing agile!!")
Anyway, thank you for putting this out there. I took a look at your first couple of chapters on Safari and your treatment of the subject is much more approachable to me than the wall of math I encountered in Leslie Lamport's stuff.
6 comments
[ 3.9 ms ] story [ 25.0 ms ] threadCan any mortals who've used TLA+ discuss their motivation for using it and the impact it had on their project? I imagine you'd have had to work in a technology-driven environment to be able to justify it to management since formal verification isn't even in the vocabulary of most ordinary development shops.
https://medium.com/espark-engineering-blog/formal-methods-in...
* A few different groups verified business ETLs with it, finding corner cases which would lose or corrupt data. Similarly, I a lot of use for deployment procedures.
* A lot of people are using it for testing optimizations: write a TLA+ spec of your system, write a spec of the optimizations, and check that they have the same behavior.
* Finding bugs in microservices. I get a _ton_ of emails about this.
* Lots of specific domain problems: trading algorithms, robotics, etc.
The main benefit of TLA+ (and formal specification in general) is that it gives you a way of both writing a precise design of your system and checking the design itself for bugs. That's something so rare in mainstream programming that many people don't even know it's possible. That's why I want to make this stuff more accessible.
Does that answer your question?
Anyway, thank you for putting this out there. I took a look at your first couple of chapters on Safari and your treatment of the subject is much more approachable to me than the wall of math I encountered in Leslie Lamport's stuff.