9 ms·

Learn TLA+

350 points by MindGods 4y ago

CuriousCosmic 4y ago
This looks awesome. I'm hoping to start working through it starting some time in the next few weeks.
bediger4000 4y ago
How does TLA compare to Spin?
- hwayne 4y ago
  The main difference is that I know how to write TLA+ and don't know how to write Spin I have the Spin book and intend to read it, but I keep having other stuff come up. It's mocking me, I know
  - bediger4000 4y ago
    The Spin book, the one with the parrot on the front, is actually pretty good. Maybe not for someone like you with deep expertise, but for almost anyone else, it has a mix of motivating anecdotes, examples, computer science and insights that I've not seen bundled up anywhere else. Your advocacy for TLA+ makes me want to try it out. I just wanted to understand what I might be getting into.
- oggy 4y ago
  I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limited C with non-deterministic choice stuck in there. TLA is a first-order logic language, and the tooling (while not great by modern language standards) felt more pleasant than Spin. It could be that you get faster model checking with Spin though, I'm not aware of any comparisons.
an_d_rew 4y ago
Awesome, thank you, Hillel! Bought the book, FWIW, and love it - but this will help me evangelize TLA+ with my employer and other groups!
dqpb 4y ago
I wish this wasn't so focused on PlusCal
- hwayne 4y ago
  In my teaching experience, more people find it easier to start with PlusCal. That said, I plan to also add a lot of topics and examples that are pure TLA+.
- ahelwer 4y ago
  They're both good to know - PlusCal for concurrent programs with more sequential if/then/else/while/for-type logic, and TLA+ for more event-driven systems that receive inputs and react with few sequential steps. Lamport has published lots of resources on TLA+ itself. I learned from Specifying Systems. I've also seen the video course and it's pretty good.
rotifer 4y ago
I just started reading the book a couple of days ago. Sigh... :-) One thing that I wish websites did is to make it easy to report simple typos and grammatical errors without having to go through GitHub. For example, on https://www.learntla.com/intro/faq.html https://www.learntla.com/intro/faq.html "losting" should be "losing". It would be great to simply and quickly report them without having to context switch and go through the overhead of opening an issue or creating a PR. (In any case, I don't even have a GitHub account.)
- hwayne 4y ago
  It's also fine to send me an email (h@mymainwebsite) or a twitter DM or whatever, I just presented the issue so people know they can send feedback and that I'll accept it.
- SloopJon 4y ago
  > I just started reading the book a couple of days ago. Sigh... :-) I wasn't even going to click the link, because I thought this was for the old online book. Because of your comment, I see that Learn TLA+ has been updated, and Hillel says of the Practical TLA+ book I bought a couple of weeks ago: "Don't bother." I haven't gotten that far yet, but I have modeled the wolf, cabbage, and goat problem, and helped the poor waiter in xkcd 287. Eventually I hope to apply it to a distributed database and our crazy Jira deployment. I'm not sure which will be harder.
  - tclancy 4y ago
    B I feel like you dropped this.
    - hwayne 4y ago
      The ISO standard for Z says it must be pronounced "Zed", even if you're American, and as revenge I now pronounce Event-B as "Event-Bed"
anonymousDan 4y ago
Several people I know with a formal methods and distributed systems background aren't that impressed with TLA+. I'm not exactly sure why or what else they prefer (Isabel? Coq?). Anyone with a formal methods background care to comment?
- ahelwer 4y ago
  It's not like TLA+ is really pushing research frontiers, it's just a great language using solid established algorithms that works really well for modeling distributed & concurrent systems. Maybe they're unhappy with the proof system part of the language? That's still a research project in progress.
- pron 4y ago
  The vast majority of people using languages like Coq, Isabelle, or Lean, are researchers, and those tools are designed for research (such as defining and exploring new logical systems). TLA+, on the other hand, is designed for practitioners, i.e. people who build systems for a living. That is why more papers are being written about Coq and Isabelle, but more bugs in more real-world systems are being found with TLA+. So it depends on what your job is.
  - avgcorrection 4y ago
  - anonymousDan 4y ago
    Yes the people I am referring to are in the business of designing and proving new distributed algorithms and proving/disproving the correctness of existing existing well-known algorithms for which only handwavy proofs have been provided. In particular it goes beyond just model checking.
    - pron 4y ago
      Right. TLA+ has a proof assistant, just as Coq and Isabelle do, and it has been used to good effect. But because there is also a model-checker capable of checking (a subset of) TLA+ (actually, two model checkers now), practitioners greatly prefer using that over a proof assistant. The reason is that if your goal isn't to publish a paper but to deploy a system, what you're optimising for is bugs found per hour of effort, and a model-checker has a higher ROI in that regard than deductive proofs.
im3w1l 4y ago
So can it spit out C or something? Or something to actually perform the algorithm? Or are you expected to manually translate back and forth between your model specification and your code?
- Jtsummers 4y ago
  It does not spit out C. TLA+ is aimed at the design/specification level, not the implementation level. You would have to take the information learned from the model checker or proof system (or even just the act of constructing the model can reveal problems) and change your program to address any discovered issues.
- philix001 4y ago
  The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec. Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.
- mhh__ 4y ago
  In practice it's fuzzy but TLA+ is meant for checking your thinking not your code as per se
tra3 4y ago
My mind works best with examples, I was about to ask here when I stumbled upon it on the TLA site [0]. The example starts out with a simple piece of code that exposes a bug, then the bug gets fixed and the following question is asked: > Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything > The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirements and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct. [0]: https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html
- gurjeet 4y ago
  I noticed a bug in the example, and thought that was the bug TLA+ would be used to solve. Apparently, that's a real bug, and the rest of the doc does not address it. So I proposed a fix for it [1]. [1]: https://github.com/hwayne/learntla-v2/pull/13 https://github.com/hwayne/learntla-v2/pull/13
  - tra3 4y ago
    Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.
  - NavinF 4y ago
    Huh you’re right! The code and the TLA+ model are different: > if (from.balance <= amount) # guard > if acct[from] >= amnt then
  - hwayne 4y ago
    God, that's embarrassing. I just merged your fix.
    - gurjeet 4y ago
      Take it easy; it's a proof that you're only human :-) This bugfix brings up 2 good points. 1. Using TLA+ is no silver bullet to writing bullet-proof code. Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. I wish there was a translator that'd convert your TLA+ to code in a language of your choice. 2. Say what people may want about centralization (Git vs. Github, etc), this successful micro-collaboration was enabled by this centralization. Someone posts a link to a book/article, someone else posts a deep-link to some example code, yet another person finds bug in the said code, hunts down the Github link, uses Github's in-place edit feature (no (`git clone` + fix + `git push`)) and submits a merge-request, the author merges the fix (and smacks head :-). All this was kicked off by a conversation on HN, a center/hub for conversations.
elcapitan 4y ago
Really liked the paper book, looking forward to the new version of the website! Nice to see some new posts on TLA every once in a while. A few days ago someone posted this series of very real-world examples: https://elliotswart.github.io/pragmaticformalmodeling/ https://elliotswart.github.io/pragmaticformalmodeling/ It's also quite good.
drekipus 4y ago
Genuine question: how does this compare versus something like modelling in primitive python? what benefits are there, or is it just a case of age and that this is language / system agnostic? I'm just finishing cosmic python[0], which talks about making a primitive model of your system first, that you can run business logic tests on, then all the other code depends upon that (domain driven design / onion layers, etc). To me it seems like this is the same thing. The only aspect that stuck out was the "two transfers at the same time" which to me, seems like it would depend on how you're implementing the model, rather than the model itself? For instance, the example in [1] could also be done in primitive python, (arguably easier to read in my opinion but I'm not used to TLA syntax :) @dataclass class Person: balance: int def wire(a: Person, b: Person, amount: int): if a.balance >= amount: a.balance -= amount b.balance += amount @pytest.mark.parametrize( "a_amount, b_amount, transfer, a_remaining, b_remaining", [ (10, 10, 10, 0, 20), # matching amount (6, 10, 10, 6, 10), # has less (0, 10, 10, 0, 10), # has nothing (10, 0, 10, 0, 10), # to empty account ], ) def test_wire(a_amount, b_amount, transfer, a_remaining, b_remaining): a = Person(balance=a_amount) b = Person(balance=b_amount) wire(a, b, transfer) assert a.balance == a_remaining assert b.balance == b_remaining The author did mention "... could be done in python" as well, so I doubt it's a case of not knowing about python, but perhaps my question is "why TLA over python?" [0]https://www.cosmicpython.com/ https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html
- pron 4y ago
  There are two parts to the answer: the expressivity of the language, and the available tools. TLA+ is not a programming language, and so cannot "run," but it is more expressive than any programming language could ever be, and can describe any discrete system at any arbitrary level of detail. This is particularly useful when the described system has some or a lot of nondeterminism, as is the case in distributed and concurrent systems. It is very easy in TLA+ to say "one of these things could happen at any time", or "the value of a variable can only grow monotonically over the system's lifetime", and it is easy to describe assertions of arbitrary complexity about a system, such as "every order that's received more than once will eventually be flagged." As for tooling, while you cannot efficiently "run" TLA+ specifications, you can check your assertions in two ways: either with the proof assistant (although that requires a lot of effort), or with a model checker, that is places more limitations on what it is that you can check but is completely automatic.
RicoElectrico 4y ago
Ah, the HN's favourite language Three Letter Acronym + I ctrl+f'd the page and the expansion of that acronym, Temporal Logic of Actions is nowhere to be found.
- hwayne 4y ago
  Leslie Lamport doesn't say what TLA+ standards for on his personal webpage, and I felt I had to pay him his respects (Real answer: it's something most of us tell you if you ask, but "Temporal logic of actions" makes it sound a lot more intimidating to learn than it actually is)
- rzzzt 4y ago
  The Glossary has it! I was also wondering how long it can go without ever resolving the meaning of each letter.
Pr0ject217 4y ago
This is very interesting and practical. Thank you.
dimal 4y ago
This looks like it could be really useful. I tend to write out my specs in pseudocode before coding anyway, so being able to easily translate that human gobbledygook into a form that can be checked for correctness, seems like it could help the creative process of coming to a solution. Just try out ideas and see if they help solve it. Keep honing them down until you get it.
metadat 4y ago
I wonder if it's possible to model how fucked up the Golang concurrency model is with TLA+? As a TLA non-SME I couldn't say, but would definitely find it useful and probably impressive. Maybe Brad Fitzpatrick could team up with Aphyr and use it to make golang v2 a bit less crap. Note: I write this with love, as someone who's written hundreds of thousands of lines of Go, and am now turned off and afraid of the behavior at the sketchy edge boundaries. I've now shifted to learning Rust, albeit slowly and finding it saddeningly challenging compared to what I can pump out with the Go. For reference, see "Data Race Patterns in Go", posted 21 days ago: https://news.ycombinator.com/item?id=31698503 https://news.ycombinator.com/item?id=31698503
- hwayne 4y ago
  I've written about this before! https://www.hillelwayne.com/post/tla-golang/ https://www.hillelwayne.com/post/tla-golang/ That said, I think the Spin syntax is slightly closer to native Go, making it easier to write specs. At least that's what people who know both Spin and Go tell me. https://github.com/dgryski/modelchecking/blob/master/spin/findall.pml https://github.com/dgryski/modelchecking/blob/master/spin/fi...
  - nextos 4y ago
    Not used Go myself, but since Go concurrency model is based on CSP, surely many CSP-based model checkers should help?
rramadass 4y ago
Also relevant: https://pron.github.io/tlaplus https://pron.github.io/tlaplus
oggy 4y ago
Thanks for your work, Hilel! I've been using TLA extensively in my job the last few months (I work at a blockchain company), and it's been a good run - we found a bunch of issues in several designs and even implemented code (some fairly critical). My secret hope is to get some co-workers to start using TLA themselves (so I can go off to do code-level verification instead hehe), I've organized a couple of internal tutorials but no takers so far - hopefully this free learning resource will help advance that goal :) On a related topic, does anyone know of a comparison to Alloy 6? I've been meaning to take a day or two to look at it (I tried Alloy out a while ago while I was still in my PhD, but have forgotten most of it), I'm curious to see how it stacks up.
evnix 4y ago
any examples of where TLA+ is being used? do any open source projects use this?
- traceroute66 4y ago
  > any examples of where TLA+ is being used? If you use Amazon AWS its pretty much guaranteed you'll be using at least one service that's been modelled using TLA+.[1] [1] https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...
sriram_malhar 4y ago
This is good stuff, Hillel. Thank you. The images don't render correctly on macOS safari (v 13.1.3). They are squished horizontally.
radicalriddler 4y ago
I wish sites like these were keyboard operable. You have a link down the bottom of the page, if I scroll to the bottom of the page (with space or down key or page down), it would be nice that it gets to the bottom, and then goes to the next page on the next keydown event. We implemented this in medical software for reading patient documents at one of my last jobs, and it's a feature I wish more sites that were focused on reading material had (docs, book replacements, etc.) Edit: just want to point out this is in no way a critique of this site specifically, so maybe off topic.
wespiser_2018 4y ago
Congrats Hillel, great work. A teammate used TLA+ at work to help diagnosis a deadlock bug due to a lock issue in postgres, and since then I've been mesmerized by its simplicity and power to prove simple invariants over complex specs. Looking forward to reading more!

Learn TLA+

350 points by MindGods 4y ago

CuriousCosmic 4y ago

This looks awesome. I'm hoping to start working through it starting some time in the next few weeks.

bediger4000 4y ago

How does TLA compare to Spin?

hwayne 4y ago
The main difference is that I know how to write TLA+ and don't know how to write Spin I have the Spin book and intend to read it, but I keep having other stuff come up. It's mocking me, I know
- bediger4000 4y ago
  The Spin book, the one with the parrot on the front, is actually pretty good. Maybe not for someone like you with deep expertise, but for almost anyone else, it has a mix of motivating anecdotes, examples, computer science and insights that I've not seen bundled up anywhere else. Your advocacy for TLA+ makes me want to try it out. I just wanted to understand what I might be getting into.
oggy 4y ago
I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limited C with non-deterministic choice stuck in there. TLA is a first-order logic language, and the tooling (while not great by modern language standards) felt more pleasant than Spin. It could be that you get faster model checking with Spin though, I'm not aware of any comparisons.

an_d_rew 4y ago

Awesome, thank you, Hillel! Bought the book, FWIW, and love it - but this will help me evangelize TLA+ with my employer and other groups!

dqpb 4y ago

I wish this wasn't so focused on PlusCal

hwayne 4y ago
In my teaching experience, more people find it easier to start with PlusCal. That said, I plan to also add a lot of topics and examples that are pure TLA+.
ahelwer 4y ago
They're both good to know - PlusCal for concurrent programs with more sequential if/then/else/while/for-type logic, and TLA+ for more event-driven systems that receive inputs and react with few sequential steps. Lamport has published lots of resources on TLA+ itself. I learned from Specifying Systems. I've also seen the video course and it's pretty good.

rotifer 4y ago

I just started reading the book a couple of days ago. Sigh... :-) One thing that I wish websites did is to make it easy to report simple typos and grammatical errors without having to go through GitHub. For example, on https://www.learntla.com/intro/faq.html https://www.learntla.com/intro/faq.html "losting" should be "losing". It would be great to simply and quickly report them without having to context switch and go through the overhead of opening an issue or creating a PR. (In any case, I don't even have a GitHub account.)

hwayne 4y ago
It's also fine to send me an email (h@mymainwebsite) or a twitter DM or whatever, I just presented the issue so people know they can send feedback and that I'll accept it.
SloopJon 4y ago
> I just started reading the book a couple of days ago. Sigh... :-) I wasn't even going to click the link, because I thought this was for the old online book. Because of your comment, I see that Learn TLA+ has been updated, and Hillel says of the Practical TLA+ book I bought a couple of weeks ago: "Don't bother." I haven't gotten that far yet, but I have modeled the wolf, cabbage, and goat problem, and helped the poor waiter in xkcd 287. Eventually I hope to apply it to a distributed database and our crazy Jira deployment. I'm not sure which will be harder.
- tclancy 4y ago
  B I feel like you dropped this.
  - hwayne 4y ago
    The ISO standard for Z says it must be pronounced "Zed", even if you're American, and as revenge I now pronounce Event-B as "Event-Bed"

anonymousDan 4y ago

Several people I know with a formal methods and distributed systems background aren't that impressed with TLA+. I'm not exactly sure why or what else they prefer (Isabel? Coq?). Anyone with a formal methods background care to comment?

ahelwer 4y ago
It's not like TLA+ is really pushing research frontiers, it's just a great language using solid established algorithms that works really well for modeling distributed & concurrent systems. Maybe they're unhappy with the proof system part of the language? That's still a research project in progress.
pron 4y ago
The vast majority of people using languages like Coq, Isabelle, or Lean, are researchers, and those tools are designed for research (such as defining and exploring new logical systems). TLA+, on the other hand, is designed for practitioners, i.e. people who build systems for a living. That is why more papers are being written about Coq and Isabelle, but more bugs in more real-world systems are being found with TLA+. So it depends on what your job is.
- avgcorrection 4y ago
- anonymousDan 4y ago
  Yes the people I am referring to are in the business of designing and proving new distributed algorithms and proving/disproving the correctness of existing existing well-known algorithms for which only handwavy proofs have been provided. In particular it goes beyond just model checking.
  - pron 4y ago
    Right. TLA+ has a proof assistant, just as Coq and Isabelle do, and it has been used to good effect. But because there is also a model-checker capable of checking (a subset of) TLA+ (actually, two model checkers now), practitioners greatly prefer using that over a proof assistant. The reason is that if your goal isn't to publish a paper but to deploy a system, what you're optimising for is bugs found per hour of effort, and a model-checker has a higher ROI in that regard than deductive proofs.

im3w1l 4y ago

So can it spit out C or something? Or something to actually perform the algorithm? Or are you expected to manually translate back and forth between your model specification and your code?

Jtsummers 4y ago
It does not spit out C. TLA+ is aimed at the design/specification level, not the implementation level. You would have to take the information learned from the model checker or proof system (or even just the act of constructing the model can reveal problems) and change your program to address any discovered issues.
philix001 4y ago
The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec. Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.
mhh__ 4y ago
In practice it's fuzzy but TLA+ is meant for checking your thinking not your code as per se

tra3 4y ago

My mind works best with examples, I was about to ask here when I stumbled upon it on the TLA site [0]. The example starts out with a simple piece of code that exposes a bug, then the bug gets fixed and the following question is asked: > Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything > The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirements and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct. [0]: https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html

gurjeet 4y ago
I noticed a bug in the example, and thought that was the bug TLA+ would be used to solve. Apparently, that's a real bug, and the rest of the doc does not address it. So I proposed a fix for it [1]. [1]: https://github.com/hwayne/learntla-v2/pull/13 https://github.com/hwayne/learntla-v2/pull/13
- tra3 4y ago
  Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.
- NavinF 4y ago
  Huh you’re right! The code and the TLA+ model are different: > if (from.balance <= amount) # guard > if acct[from] >= amnt then
- hwayne 4y ago
  God, that's embarrassing. I just merged your fix.
  - gurjeet 4y ago
    Take it easy; it's a proof that you're only human :-) This bugfix brings up 2 good points. 1. Using TLA+ is no silver bullet to writing bullet-proof code. Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. I wish there was a translator that'd convert your TLA+ to code in a language of your choice. 2. Say what people may want about centralization (Git vs. Github, etc), this successful micro-collaboration was enabled by this centralization. Someone posts a link to a book/article, someone else posts a deep-link to some example code, yet another person finds bug in the said code, hunts down the Github link, uses Github's in-place edit feature (no (`git clone` + fix + `git push`)) and submits a merge-request, the author merges the fix (and smacks head :-). All this was kicked off by a conversation on HN, a center/hub for conversations.

elcapitan 4y ago

Really liked the paper book, looking forward to the new version of the website! Nice to see some new posts on TLA every once in a while. A few days ago someone posted this series of very real-world examples: https://elliotswart.github.io/pragmaticformalmodeling/ https://elliotswart.github.io/pragmaticformalmodeling/ It's also quite good.

drekipus 4y ago

Genuine question: how does this compare versus something like modelling in primitive python? what benefits are there, or is it just a case of age and that this is language / system agnostic? I'm just finishing cosmic python[0], which talks about making a primitive model of your system first, that you can run business logic tests on, then all the other code depends upon that (domain driven design / onion layers, etc). To me it seems like this is the same thing. The only aspect that stuck out was the "two transfers at the same time" which to me, seems like it would depend on how you're implementing the model, rather than the model itself? For instance, the example in [1] could also be done in primitive python, (arguably easier to read in my opinion but I'm not used to TLA syntax :) @dataclass class Person: balance: int def wire(a: Person, b: Person, amount: int): if a.balance >= amount: a.balance -= amount b.balance += amount @pytest.mark.parametrize( "a_amount, b_amount, transfer, a_remaining, b_remaining", [ (10, 10, 10, 0, 20), # matching amount (6, 10, 10, 6, 10), # has less (0, 10, 10, 0, 10), # has nothing (10, 0, 10, 0, 10), # to empty account ], ) def test_wire(a_amount, b_amount, transfer, a_remaining, b_remaining): a = Person(balance=a_amount) b = Person(balance=b_amount) wire(a, b, transfer) assert a.balance == a_remaining assert b.balance == b_remaining The author did mention "... could be done in python" as well, so I doubt it's a case of not knowing about python, but perhaps my question is "why TLA over python?" [0]https://www.cosmicpython.com/ https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html

pron 4y ago
There are two parts to the answer: the expressivity of the language, and the available tools. TLA+ is not a programming language, and so cannot "run," but it is more expressive than any programming language could ever be, and can describe any discrete system at any arbitrary level of detail. This is particularly useful when the described system has some or a lot of nondeterminism, as is the case in distributed and concurrent systems. It is very easy in TLA+ to say "one of these things could happen at any time", or "the value of a variable can only grow monotonically over the system's lifetime", and it is easy to describe assertions of arbitrary complexity about a system, such as "every order that's received more than once will eventually be flagged." As for tooling, while you cannot efficiently "run" TLA+ specifications, you can check your assertions in two ways: either with the proof assistant (although that requires a lot of effort), or with a model checker, that is places more limitations on what it is that you can check but is completely automatic.

RicoElectrico 4y ago

Ah, the HN's favourite language Three Letter Acronym + I ctrl+f'd the page and the expansion of that acronym, Temporal Logic of Actions is nowhere to be found.

hwayne 4y ago
Leslie Lamport doesn't say what TLA+ standards for on his personal webpage, and I felt I had to pay him his respects (Real answer: it's something most of us tell you if you ask, but "Temporal logic of actions" makes it sound a lot more intimidating to learn than it actually is)
rzzzt 4y ago
The Glossary has it! I was also wondering how long it can go without ever resolving the meaning of each letter.

Pr0ject217 4y ago

This is very interesting and practical. Thank you.

dimal 4y ago

This looks like it could be really useful. I tend to write out my specs in pseudocode before coding anyway, so being able to easily translate that human gobbledygook into a form that can be checked for correctness, seems like it could help the creative process of coming to a solution. Just try out ideas and see if they help solve it. Keep honing them down until you get it.

metadat 4y ago

I wonder if it's possible to model how fucked up the Golang concurrency model is with TLA+? As a TLA non-SME I couldn't say, but would definitely find it useful and probably impressive. Maybe Brad Fitzpatrick could team up with Aphyr and use it to make golang v2 a bit less crap. Note: I write this with love, as someone who's written hundreds of thousands of lines of Go, and am now turned off and afraid of the behavior at the sketchy edge boundaries. I've now shifted to learning Rust, albeit slowly and finding it saddeningly challenging compared to what I can pump out with the Go. For reference, see "Data Race Patterns in Go", posted 21 days ago: https://news.ycombinator.com/item?id=31698503 https://news.ycombinator.com/item?id=31698503

hwayne 4y ago
I've written about this before! https://www.hillelwayne.com/post/tla-golang/ https://www.hillelwayne.com/post/tla-golang/ That said, I think the Spin syntax is slightly closer to native Go, making it easier to write specs. At least that's what people who know both Spin and Go tell me. https://github.com/dgryski/modelchecking/blob/master/spin/findall.pml https://github.com/dgryski/modelchecking/blob/master/spin/fi...
- nextos 4y ago
  Not used Go myself, but since Go concurrency model is based on CSP, surely many CSP-based model checkers should help?

rramadass 4y ago

Also relevant: https://pron.github.io/tlaplus https://pron.github.io/tlaplus

oggy 4y ago

Thanks for your work, Hilel! I've been using TLA extensively in my job the last few months (I work at a blockchain company), and it's been a good run - we found a bunch of issues in several designs and even implemented code (some fairly critical). My secret hope is to get some co-workers to start using TLA themselves (so I can go off to do code-level verification instead hehe), I've organized a couple of internal tutorials but no takers so far - hopefully this free learning resource will help advance that goal :) On a related topic, does anyone know of a comparison to Alloy 6? I've been meaning to take a day or two to look at it (I tried Alloy out a while ago while I was still in my PhD, but have forgotten most of it), I'm curious to see how it stacks up.

evnix 4y ago

any examples of where TLA+ is being used? do any open source projects use this?

traceroute66 4y ago
> any examples of where TLA+ is being used? If you use Amazon AWS its pretty much guaranteed you'll be using at least one service that's been modelled using TLA+.[1] [1] https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...

sriram_malhar 4y ago

This is good stuff, Hillel. Thank you. The images don't render correctly on macOS safari (v 13.1.3). They are squished horizontally.

radicalriddler 4y ago

I wish sites like these were keyboard operable. You have a link down the bottom of the page, if I scroll to the bottom of the page (with space or down key or page down), it would be nice that it gets to the bottom, and then goes to the next page on the next keydown event. We implemented this in medical software for reading patient documents at one of my last jobs, and it's a feature I wish more sites that were focused on reading material had (docs, book replacements, etc.) Edit: just want to point out this is in no way a critique of this site specifically, so maybe off topic.

wespiser_2018 4y ago

Congrats Hillel, great work. A teammate used TLA+ at work to help diagnosis a deadlock bug due to a lock issue in postgres, and since then I've been mesmerized by its simplicity and power to prove simple invariants over complex specs. Looking forward to reading more!