10 ms·
Learn TLA+ (2018)
- hwayne 8y agoGodDAMN am I behind on updating this There's at least a couple more major improvements I want to make. One is fixing all of the small errors, and one is adding c-syntax. They've been stalled out due to Reasons (tm), but I'm hoping on diving back in soon.
- duality 8y agoRegardless, thanks for the informative site.
- brodo 7y agoThere is C syntax? Neat. Is it used in your book?
- strangecasts 7y agoPractical TLA+ uses the Pascal-style syntax for PlusCal - the only guide to the C syntax that comes to mind ATM is Lamport's own: https://lamport.azurewebsites.net/tla/c-manual.pdf https://lamport.azurewebsites.net/tla/c-manual.pdf
- hwayne 7y agoI really strongly prefer the p-style syntax because it doesn't overload the meaning of `{}`, but a lot of other people in the community use c-style.
- asimpletune 8y agoLamport also made a free video series for learning TLA+ http://lamport.azurewebsites.net/video/videos.html http://lamport.azurewebsites.net/video/videos.html
- dqpb 7y agoThese videos are great!
- lewis1028282 8y agoIs this like formal verification/formal methods then?
- chimpburger 8y agoIt is a formal method.
- timClicks 8y agoLeslie Lamport has provided his own +1 to this book, as well as a thorough review here https://lamport.azurewebsites.net/tla/practical-tla.html https://lamport.azurewebsites.net/tla/practical-tla.html
- moocowtruck 8y agooh wow that was really awesome for him to do that! really appreciate you posting this link
- dqpb 8y agoCan someone who has learned TLA+ comment on how useful it is has been for you?
- mavelikara 8y agoSomeone from AWS posted this few days ago: https://news.ycombinator.com/item?id=19634915 https://news.ycombinator.com/item?id=19634915
- k__ 8y agoIs this somehow integrated with Java or does it work with a programming language of my choice?
- strangecasts 8y agoSpecifications aren't tied to any specific programming language - you're outlining how the algorithm should work, not the implementation. (You can write Java code and invoke it during model-checking if you really need to, but I haven't come across any situation where it's actually necessary.)
- k__ 7y agoAh, okay. I had the impression it was about somehow writing a program in a more strict language and then exporting it to Java. I don't do much algorithmic design.
- hwayne 8y agoI've written specifications of Ruby and Python codebases before, and worked with people who wrote Java, C, and Haskell code. It's pretty versatile!
- raegis 8y agoI spent a 6 month parental leave learning it and experimenting with it. I enjoyed writing specifications so much that I thought programming was a waste of time. You should watch the video lectures. The first 2 or 3 will get you going. A first simple exercise might be to specify the least common multiple following Lamport's GCD example. I'm a math major, by the way.
- daenz 8y agoEvery time I see some TLA+ related article, I read it and then spend an hour convincing myself that I don't have time to learn it right now, even though I really want to. That convincing usually comes in the form of showing that the gains are not worth the effort for the software field that I am in. Can someone change my mind on this?
- jononor 8y agoWhat software field are you in?
- daenz 8y agoGeneral, non-critical software systems. My understanding about TLA+ was that it really shines in critical software systems where the result of the system crashing would be catastrophic. The effort involved in modelling the non-critical systems I work on never seems to outweigh the effort of "write a test, fix the bug, re-deploy"
- nickpsecurity 8y agoIt's good for temporal errors, like ordering or concurrency. Those are often the hardest bugs to track down with inspection or testing. Model-checkers such as TLA+ can find them fast. Formal specifications themselves have a few benefits. The first is they force you to make everything explicit that's usually a hidden assumption. From there, they might check the consistency of your system. From there, you might analyze them or generate code from the specs. Spotting hidden or ambiguous assumptions plus detecting interface errors were main benefits in industrial projects going back decades. However, you can get a taste of the benefits by combining Design-by-Contract with contract/property/spec-based testing and runtime checks. Design-by-Contract is a lot like asserts. Should be easy to learn with more obvious value. I'll also note that tools such as Frama-C and SPARK Ada used with code proving are adding or did add the ability to turn all the specs/contracts into runtime checks. So, that's already available in open source or commercial form. And anything you can't spec, just write tests for. :) https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
- dqpb 8y agoThe syntax in that first example is off putting.
- pron 8y agoTLA+ uses an almost-standard mathematical notation, so that people with some familiarity with mathematics can read it in ~10 minutes of training. You can see examples of what it looks like in my post here (https://pron.github.io/posts/tlaplus_part2 https://pron.github.io/posts/tlaplus_part2) This website chooses to show the ASCII version that you actually type to get the "real" pretty-printed syntax.
- jnwatson 8y agoYes, you can definitely tell the inventor of TLA was also the first developer of LaTeX. As such, it is a language best read after typesetting. For a good example, see Appendix B in Diego Ongaro's dissertation [1], the formal Raft specification. After a little of the Learn TLA+ book, I was able to muddle through the spec enough to implement it. 1: https://ramcloud.stanford.edu/~ongaro/thesis.pdf https://ramcloud.stanford.edu/~ongaro/thesis.pdf
- karl_schlagenfu 8y agoHow does this compare with other formal methods like Z? Has anyone here used them successfully in the field?
- fizwhiz 8y agoSince the author hangs out here on HN, I'd like to ask: how long does it take to develop a working proficiency to model standard distributed systems (ex: a souped up key/value store)? It seems like he's written 2 books: Learn TLA+ Practical TLA+ Would there be any other resources that you'd recommend to supplement after those 2 books?
- pron 8y agoNot the author, but it would take 2-3 weeks if you learn by yourself (to get real stuff done, not to be an expert), or 3 full days of hands-on training. I would recommend Lamport's video course[1] and TLA+ hyperbook[2] (Lamport says he's stopped working on it, but it's fairly complete). Note that both Learn TLA+ and Practical TLA+ don't teach much of TLA+, but rather a language called PlusCal that compiles to TLA+. Some programmers may find it easier to start with because, unlike TLA+, PlusCal resembles a programming language (and like all programming languages, it is much more complex than TLA+, but more familiar). Hillel's book also contains some good real-life examples. You can also find examples and various other links posted on the TLA+ subreddit[3]. [1]: http://lamport.azurewebsites.net/video/videos.html http://lamport.azurewebsites.net/video/videos.html [2]: http://lamport.azurewebsites.net/tla/hyperbook.html http://lamport.azurewebsites.net/tla/hyperbook.html [3]: https://www.reddit.com/r/tlaplus/ https://www.reddit.com/r/tlaplus/
- nickpsecurity 8y ago"Note that both Learn TLA+ and Practical TLA+ don't teach much of TLA+, but rather a language called PlusCal that compiles to TLA+. Some programmers may find it easier to start with because, unlike TLA+, PlusCal resembles a programming language" Most evidence indicates using familiar concepts aids learning. That makes me hypothesize the best recommendation is the more mathematical ones for folks strong in math and the programmer-centric ones for those strong in that. That also implies that, for each of these formal topics, we need one version for each audience to draw more people in.
- fizwhiz 7y ago
- akersten 8y agoIn the landing page example: > But if we run the model checker, we find that’s not true: Alice could trade an item to herself and, before that process finishes running, resolve a parallel trade giving that same item to Bob. Then the first trade resolves and Alice gets the item back. How does the model checker know that "parallel threads" are even a possibility here? It seems like it's checking what amounts to a leaky abstraction from the actual implementation of this algorithm. In my mind a strictly logical validator would look at the proposed algorithm and say it checks out (since in math-land transactions are atomic). Is this just a feature of the model checker? Can it be turned off/tuned to the expected real-world implementations of the algorithm?
- loup-vaillant 8y agoTLA+ is originally mainly meant to check for concurrency bugs, so the possibility of parallel threads is kind of in its core DNA. The name "process" might also give a hint that parallel threads are indeed possible. I don't know how, but I expect you can indeed model actual transactions.
- hwayne 8y agoDepends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transaction by determining the changes that the overall transaction makes and then declaring them all as part of a single action.
- gmfawcett 8y agoIt's a feature. When you specify the algorithm, you also specify which actions are atomic, and which aren't.
- strangecasts 8y agoPlusCal 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] https://learntla.com/concurrency/labels/ https://learntla.com/concurrency/labels/ [2] https://youtu.be/_9B__0S21y8?t=955 https://youtu.be/_9B__0S21y8?t=955 (15:55)
- mjfl 8y agoWhat is the difference between formal methods as implemented by TLA+, proof assistants like Coq, and theorem proving languages like Agda (Idris?)?
- jlrubin 8y agocoq allows you to extract a real program, whereas TLA+ just checks a spec for correctness (and you may have bugs implementing it)
- pron 8y agoSee my other comment on the matter, but this presents a choice where there is none. No tool that extracts or verifies actual code (and people have actually done both with TLA+) can operate on programs larger than a few thousand lines. So it's not a choice between fully verifying a 200KLOC program or just its 2000-line high-level spec. It's between verifying/extracting a 2000 line program or a 2000 line spec that abstracts a 200KLOC program. In other words, for programs of a certain size, verifying a high-level spec is the only real option for "deep" verification.
- hwayne 8y agoI've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages: 1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want) 2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck. Of course extraction has its own benefits. Coq is a pretty cool tool :)
- 0815test 8y agoTLA+ uses model checking over what can be understood as a custom modal logic-- the latter means that TLA is basically adding a bunch of modalities (which could also be understood as (co-)monads) that allow for the modeling of state ("temporal" logic), nondeterminism (which also shows up in the modeling of abstraction/refinement relations) and perhaps some other features, over the basic logic that you would find pre-defined in most theorem provers. The use of model checking means that TLA+ is basically a glorified fuzzer: it will attempt to find a refutation of the model you define (such a model, in turn is usually an abstraction of the system you actually care about; not something that gets verified "end-to-end" like in Agda or Coq) and any such refutation will be a genuine proof that the model fails in some way; but a failure to find one does not amount to a proof of correctness!
- dorfsmay 8y agoIs Formal Specification used by proving language like Coq and Idris? Are they a different way of doing the same thing? Or two completely different thing?
- pron 8y agoThey share many philosophical similarities, but their design and goals are very different. Coq and Idris are mostly used for research. TLA+ is designed for heavy-duty, everyday use in industry by software and hardware developers working on large, complex real-world systems.
- youeseh 8y agoSo, like writing code and then writing tests for it?
- chimpburger 8y agoNot really. Formal verification methods are mathematically rigorous. They can mathematically prove or disprove correctness of programs and catch bugs that would be extremely difficult for a human to find https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification
- youeseh 8y ago"Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior." It sounds a lot like writing your specs as tests that are then satisfied by the implementation code.
- deleted 8y ago[deleted]
- chimpburger 8y agoTLA+ is for building and verifying a formal model of the program (a blueprint), not for verifying the implementation.
- endiangroup 8y agoWe used this resource to put together a model for our distributed sessions management algorithm, heres a GitHub with Go implementation and PlusCal / TLA+ model [1]. We also wrote a more in depth article about it here [2] (with an interactive version in JS). It took a few attempts but eventually it clicked! [1] https://github.com/endiangroup/compandauth https://github.com/endiangroup/compandauth [2] https://endian.io/articles/compandauth/ https://endian.io/articles/compandauth/
- OptionX 8y agoWhat's the advantage of this versus normal unit testing?
- strangecasts 8y agoThey're complementary, IMO: unit tests show that your implementation works as expected, while a formal specification allows you to check that your approach is right to begin with. That being said, TLA+ specifications have uncovered really hairy concurrency bugs which would be a nightmare to unit test - for instance, Amazon found bugs in DynamoDB which required 35 steps to reproduce [1]. [1] http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p...
- mirceal 8y agounit testing (and any kind of testing for that matter) shows that your code works for a set of inputs. formal verification methods show that it works for all inputs. it’s the holy grail but comes with a really high price tag to actually do it (so unless you’re writing something critical or have a lot of resources you normally get your software to the point where it’s good enough through unit/etc testing)
- duality 8y agoThink of a process by which you start with a vague sketch of a system and end up with a concrete implementation in, say, C++. The latter is the highest level and least detailed. The latter is as detailed as the specification of your system will get. A prose design document of your model might sit somewhere on this spectrum very close to the vague sketch. A TLA+ spec sits somewhere in the middle. It's a refinement of the design doc with more details specified concretely, but not all of them (that's the actual implementation). But this mid-level specification is usually enough to make highly non-trivial assertions that invariants hold (safety properties) and also liveness properties are satisfied too. But keep in mind that the specification of your system is distinct from the model checking of that spec. The latter is like a test, albeit of your system not just some "unit" within your system.
- jnwatson 8y agoI guess this is a meta question: do typical US undergraduate university Computer Science curricula not have Formal Methods as a class? I'm just wondering because of the number of fairly basic questions here. I went to a middling midwestern state school 20ish years ago and that was part of the curriculum. Perhaps we have lots of non-CS-graduates here? This is not to denigrate the discussion. I'm just surprised that this is news.
- macintux 8y agoI never completed my degree, but even at a very math-centric CS program I don’t remember seeing a formal methods class. OTOH my recall of a curriculum from 15-20 years ago should not be relied upon.
- ajxs 8y agoWhile it seems anecdotally true that the mathematical foundations of computer science are being downplayed in universities in favour of giving students a more practical education in software engineering, which is an entire contentious discussion in and of itself. I think that a big factor in influencing your observation could be that CS is no longer the main entry point into a career in software development. In the organisation I work in, many of the younger hires do not come from CS backgrounds, and even many of the older hires come from other scientific disciplines.
- momofarm 8y agoif you want to get into software development, just go to any so called "boot-camp" class for few couple months. Then you know how to write some webpages with new shiny JS framework, congrats you are a "qualified" software guy. Now go to write those sh*ty code ............ Math? what math? CS background? algorithm? if you are not going to challenge FAAG why bothered? if you just want to code few pages, writing some sql query, there is no need for that. and for 80% of enterprises, they need only CHEAP engineers. sorry for the rant, just another morning with lots of idiots bothered me.
- ajxs 8y ago
- GTP 7y agoIs there a validator to verify if an implementation of an algorithm respects the TLA+ specification? Can somebody please tell me (some of) the main differences between TLA+ and JML?
- 0815test 7y ago> Is there a validator to verify if an implementation of an algorithm respects the TLA+ specification? TLA+ has some tools to do this, if you write your implementation in some TLA+-specific language like PlusCal. But this would be the sort of "end-to-end" verification that TLA+ proponents would regard as only being feasible for relatively simple software. Relatedly, JML basically adds support for "design by contract" specifications to the Java programming language - expressing preconditions, postconditions and invariants. These can be quite useful, but the focus with TLA+ - in this thread and elsewhere - seems to be rather on "deeper" properties that encompass entire systems in a more global and cross-cutting way, and are thus inherently harder to manage with simpler tools.
- acrophiliac 7y agoDisappointed. Was expecting to learn more about Three Letter Acronyms. :)
- skadamat 7y agoHillel Wayne was recently on the Future of Coding podcast and they go deep into formal methods - https://futureofcoding.org/episodes/038 https://futureofcoding.org/episodes/038
- billfruit 7y agoWhen I did spend a little amount of time trying to learn TLA+, the biggest annoyance is the two different syntax/form in which TLA+ can be written, a mathematical symbolic form, and a text form like a program. Now, this topic is a rather abstract and difficult to comprehend one, and having two equivalent ways of doing it, introduced right from the beginning, I thought was too much of a cognitive load, considering the difficulty of the subject. I hope this material from the article is simpler for learners.