4 ms·

i've encountered TLA before and am a complete newb. That being said, I've wanted to use it for modeling distributed systems but felt the learning curve was too

i've encountered TLA before and am a complete newb. That being said, I've wanted to use it for modeling distributed systems but felt the learning curve was too steep. Now many years later, I think i'm finally going to take another go. Would love to know where the TLA community hides. I dont see much real info on it in the wild.

Jtsummers 8y ago
https://groups.google.com/forum/#!forum/tlaplus https://groups.google.com/forum/#!forum/tlaplus This is the Google group and it has Lamport and others chiming in with answers to questions regularly. Though it's not terribly active. https://www.reddit.com/r/tlaplus/ https://www.reddit.com/r/tlaplus/ The subreddit for it. Hillel Wayne (author of this article) and Ron Pressler (pron here, pron98 on reddit) both frequent the site and post content to it. It's not terribly active, but it exists. I think this is something that doesn't quite have a widespread and public community. Which is unfortunate, but it's just advanced enough for many to feel it's beyond them, and just abstract enough for others to feel it has no (or very limited) utility. I will recommend exploring it though. I spent some time about 2 or 3 years back learning it to a moderate degree and successfully applied it to some problems at work. Though I haven't used it much since then.
BoiledCabbage 8y ago
Haven't used it, but this site looks like a great resource and is in my queue to go through. https://learntla.com/introduction/ https://learntla.com/introduction/
- Jtsummers 8y ago
  I was working on gathering my links and that was one I was going to suggest. It's a very approachable intro, and also written by Hillel. I've added his (now published) book to my queue to purchase and read through. I may do that sooner rather than later so I can provide feedback here on other discussions regarding it, beyond saying that it exists. The talk linked at the top of that page is pretty good as well as a tutorial, though hardly complete. As I recall he presents his examples well and has good motivating examples for using TLA+ in it.
pron 8y ago
> Would love to know where the TLA community hides. Currently, the (tiny) community hides mostly in large companies and doesn't blog or evangelize much. Nevertheless, because it is used in such large companies on such critical and popular systems, its direct impact is far larger than that of say, Haskell, despite fewer people knowing it. Here is a talk[1] about Microsoft's experience with TLA+. They do a three-day workshop for developers, which is sufficient to specify and verify the design of large, complex, real-world systems. [1]: https://youtu.be/ifFfxRCX_jw https://youtu.be/ifFfxRCX_jw

Jtsummers 8y ago

https://groups.google.com/forum/#!forum/tlaplus https://groups.google.com/forum/#!forum/tlaplus This is the Google group and it has Lamport and others chiming in with answers to questions regularly. Though it's not terribly active. https://www.reddit.com/r/tlaplus/ https://www.reddit.com/r/tlaplus/ The subreddit for it. Hillel Wayne (author of this article) and Ron Pressler (pron here, pron98 on reddit) both frequent the site and post content to it. It's not terribly active, but it exists. I think this is something that doesn't quite have a widespread and public community. Which is unfortunate, but it's just advanced enough for many to feel it's beyond them, and just abstract enough for others to feel it has no (or very limited) utility. I will recommend exploring it though. I spent some time about 2 or 3 years back learning it to a moderate degree and successfully applied it to some problems at work. Though I haven't used it much since then.

BoiledCabbage 8y ago

Haven't used it, but this site looks like a great resource and is in my queue to go through. https://learntla.com/introduction/ https://learntla.com/introduction/

Jtsummers 8y ago
I was working on gathering my links and that was one I was going to suggest. It's a very approachable intro, and also written by Hillel. I've added his (now published) book to my queue to purchase and read through. I may do that sooner rather than later so I can provide feedback here on other discussions regarding it, beyond saying that it exists. The talk linked at the top of that page is pretty good as well as a tutorial, though hardly complete. As I recall he presents his examples well and has good motivating examples for using TLA+ in it.

pron 8y ago

> Would love to know where the TLA community hides. Currently, the (tiny) community hides mostly in large companies and doesn't blog or evangelize much. Nevertheless, because it is used in such large companies on such critical and popular systems, its direct impact is far larger than that of say, Haskell, despite fewer people knowing it. Here is a talk[1] about Microsoft's experience with TLA+. They do a three-day workshop for developers, which is sufficient to specify and verify the design of large, complex, real-world systems. [1]: https://youtu.be/ifFfxRCX_jw https://youtu.be/ifFfxRCX_jw