[HN Gopher] Learn TLA+
___________________________________________________________________
Learn TLA+
Author : MindGods
Score : 107 points
Date : 2022-07-01 20:48 UTC (2 hours ago)
(HTM) web link (www.hillelwayne.com)
(TXT) w3m dump (www.hillelwayne.com)
| bediger4000 wrote:
| How does TLA compare to Spin?
| anonymousDan wrote:
| 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?
| mhh__ wrote:
| TLA+ has very different aims.
|
| A better criticism would probably be to note that TLA+ is even
| within the more similar world of (say) model checking, it is a
| LISP to (say) Spin's (or similar) C
| [deleted]
| ahelwer wrote:
| 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 wrote:
| 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 wrote:
| hwayne wrote:
| I'd be interested in hearing their opinions! Do you know more
| about their contexts? Like if they're in academia, industry,
| what kinds of things they're doing, etc.
|
| (I don't think it's necessarily the case that they prefer
| Isabelle or Coq; it really depends on what they're trying to
| do. I'd be especially fascinated if they prefer, say, SPIN to
| TLA+, which is a much closer tool.)
| an_d_rew wrote:
| Awesome, thank you, Hillel!
|
| Bought the book, FWIW, and love it - but this will help me
| evangelize TLA+ with my employer and other groups!
| jacoblambda wrote:
| This looks awesome. I'm hoping to start working through it
| starting some time in the next few weeks.
| dqpb wrote:
| I wish this wasn't so focused on PlusCal
| hwayne wrote:
| 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 wrote:
| 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.
| im3w1l wrote:
| 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 wrote:
| 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.
| rotifer wrote:
| 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
| "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 wrote:
| 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.
| elcapitan wrote:
| 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/ It's also
| quite good.
| tra3 wrote:
| 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
___________________________________________________________________
(page generated 2022-07-01 23:00 UTC)