"Tackling Concurrency Bugs with TLA+" by Hillel Wayne
Why Hacker News recommends it
Recommended as a concise, high-level intro to what TLA+ is and when it helps.
What it is
Hillel Wayne's Strange Loop talk introducing TLA+ as a specification language for finding concurrency bugs in designs. It covers stalling, race conditions and dropped messages, with PlusCal examples.
Recommended by 3 HN commenters across 3 different months, 2018 to 2025.
What Hacker News said
Recommends ajmurmann · 2018-03 · on “Modeling Redux with TLA+”
Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: [this video] If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.
Recommends bandwitch · 2018-07 · on “Learn how to design large-scale systems”
I feel TLA+ would be too much to ask in a system interview which is what this site is about. In case anybody is interested, there is a nice talk by Hillel Wayne on youtube ( [this video] ) that provides a high-level overview on what TLA+ is about.
Recommends cess11 · 2025-05 · on “The first year of free-threaded Python”
The literature on distributed systems is huge. It depends a lot on your use case what you ought to do. If you're lucky you can avoid shared state, as in no race conditions in either end of your executions. [this video] is fairly concise and gives some recommendations for literature and techniques, obviously making an effort in promoting PlusCal/TLA+ along the way but showcases how even apparently simple algorithms can be problematic as well as how deep analysis has to go to get you a guarantee that the execution will be bug free.
Cites hwayne · 2018-03 · on “Ask HN: Anyone ever use TLA+ on a Webapp”
I've used it for caching, batch processing, and concurrent web apps, and it's been a huge help. I've gone into how I used it in a couple of places: - "Tackling Concurrency Bugs with TLA+" ( [this video] ) - "Formal Methods in Practice" ( [LINK] ) I love helping people with this stuff, so ping me if you have any questions!
Cites strangecasts · 2019-04 · on “Learn TLA+ (2018)”
PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start off with a very simple spec with totally atomic transactions, and gradually make it more granular by introducing more labels, as shown in Wayne's Strange Loop presentation [2] [1] [LINK] [2] [this video] (15:55)