Specifying systems
by Leslie Lamport · first published 2002
75% recommend21% neutral4% critical
Why HN recommends it
Authoritative TLA+ reference by its creator, free online, building from propositional and predicate logic to temporal logic and covering the TLC model checker; suits readers learning to specify concurrent systems.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
2019–2026Practical TLA+
Hillel Wayne
Recommended by 15 · mentioned by 2015 recommend · 20 mention15 recommend · 2015 recommend
Software Foundations
Benjamin C. Pierce
Recommended by 58 · mentioned by 6058 recommend · 60 mention58 recommend · 6058 recommend
2007–2026How to prove it
Daniel J. Velleman
Recommended by 78 · mentioned by 10478 recommend · 104 mention78 recommend · 10478 recommend
2007–2026I Am a Strange Loop
Douglas R. Hofstadter
Recommended by 101 · mentioned by 204101 recommend · 204 mention101 recommend · 204101 recommend
2008–2026Elements
Euclid
Recommended by 60 · mentioned by 22560 recommend · 225 mention60 recommend · 22560 recommend
2007–2026The art of computer programming
Donald Knuth
Recommended by 336 · mentioned by 1,125336 recommend · 1,125 mention336 recommend · 1,125336 recommend
For me, there’s no better explanation possible than the description of software behavior in Specifying Systems by Leslie Lamport: > Formally, we define a behavior to be a sequence of states, where a state is an assignment of values to variables. We specify a system by specifying a set of possible behaviors—the…
on “Reconsidering the way I explain programming (2020)” ↗If you're interested in learning TLA+, the best resources are: (1) Specifying Systems by Leslie Lamport (https://lamport.azurewebsites.net/tla/book.html) This is the original TLA+ textbook (I myself learned from it) and is very thorough, but sometimes fails to differentiate between specs…
on “Building a “Simple” Distributed System – Formal Verification” ↗…and guide as you start specifying your own systems [2]. It has a number of examples and projects to work on. Eventually if you want to go deep after you've decided it's worth it for yourself, get into Specifying Systems the text book and bible of TLA+ [3]. Program Synthesis has a lot of research in it and is starting to show promising results. I'd say that while the research has been going on for a long time it's still…
on “Keeping CALM: when distributed consistency is easy” ↗…Amazon to check designs for their distributed algorithms. They have used it to check parts of S3 for example: https://lamport.azurewebsites.net/tla/formal-methods-amazon.... Best reference is the book Specifying Systems: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf. Then you have theorem provers / proof assistants based on type theory. These are frankly complex, but getting better. F*: This one is the most…
on “Coverage is not strongly correlated with test suite effectiveness” ↗Read Leslie Lamport's Specifying Systems (2003),¹ study the example modules, study others' modules online, and write your own. It's a really good way to bug test your program's logic before you choose the language to code it in. It's not easy…
on “Ask HN: How to get good at building functional prototypes fast” ↗For anybody interested in this field: Specifying Systems by Leslie Lamport, the same guy that gave us Logical Clocks and Paxos (free on Ms Reseach website): http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
on “Hacker-Proof Code Confirmed” ↗What do you mean by "run"? Check in the TLC model checker? You need to first write a configuration that you want to check. Lamport's Specifying Systems has full documentation for using the model checker from the command line. But if you're a beginner, you might be better off using the IDE, at least at first, as it helps you write a configuration very…
on “Verdi – Formally Verifying Distributed Systems (2016)” ↗…formulation looks good. I was so happy to get your advice that I bought a copy of Practical TlA+ from Apress. Even if it doesn't help with this particular project, I'm sure it will be useful down the line. Specifying Systems has been my go-to reference alongside Lamport's video tutorial. Thanks for suggesting Chapter 7 of the Hyperbook - I never thought to look there. EDIT: I misread: Chapter 7 refers to the chapter in Practical…
on “TLA+: design, model, document, and verify concurrent systems” ↗…Processes. Tony Hoare. This book is surprising in its compactness and lucidity. Pi Calculus. Robin Milner. Semantics With Applications. Hanne Riis Nielson On Concurrent Programming. Fred Schneider. Specifying Systems with TLA+. Leslie Lamport. Distributed Algorithms. Nancy Lynch. Reliable Distributed Computing. Ken Birman and Robert Van Renesse. I'm sure I'll recall more as soon as I hit "reply".
on “Structure and Interpretation of Computer Programs (1996) [pdf]” ↗…are blending complex systems that had never interacted together before with the expectation that they collaborate forming a single, larger system." I suggest more people read the first few chapters of Specifying Systems by Lamport. Maybe the rest is good also, but that's as far as I got. It works through a trivial system (display clock) and combines it with another trivial system (display weather). Nothing Earth-shattering,…
on “Blending complex systems made my latency 10x higher” ↗Practical TLA+ is indeed a great place to start, and Hillel Wayne's writing out formal methods is all worth reading. Lamport's TLA+ book, and "Specifying Systems" are both available online (https://lamport.azurewebsites.net/tla/book.html). That one's worth a read too. Lamport's approach to teaching TLA+ is different, and probably more suited to the mathematically-inclined.…
on “How Amazon Web Services Uses Formal Methods (2015) [pdf]” ↗…with spending the past several years trying to take it as seriously as possible. Other good sources are McCarthy’s Situation Calculus and all of the stuff that Lamport has written on on TLA+ (especially Specifying Systems[1]). The big idea behind scalability (IMO) is that we want the pain of maintaining a system to grow logarithmically with respect to the size of the system. Now, size can mean many things (number of customers,…
on “Roy Fielding's Misappropriated REST Dissertation” ↗I would add an excellent introduction by Scott Wlaschin on YouTube called "Building confidence in concurrent code using a model checker."[0] Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two…
on “TLA+ Action Properties” ↗…Methods by Monin. * Introductory Logic and Sets for Computer Scientists by Nimal Nissanke. * Mathematical Notation: A Guide for Engineers and Scientists by Scheinerman. This allowed me to start studying Specifying Systems by Leslie Lamport which is the main book for TLA+. PS: User "pron" to whom you replied to has a nice 4-part series on TLA+ which i have linked to in another post in this thread. He really knows this…
on “TLA+ is hard to learn (2018)” ↗…that he's a very prolific writer and speaker, in addition to contributing to a fairly diverse set of Computer Science fields. I usually enjoy Lamport's speeches, and I have said before that his book Specifying Systems should be mandatory reading for nearly anyone interested in CS, due to how approachable it is, and yet how deep it goes.
on “Paxos” ↗