I have actually been going through Practical TLA+ and enjoying it, though honestly sometimes it’s a bit hard to go from “I know that this business problem should be modelable” to “here is a sensible model for the problem”.
I know that it’s not actually super important but just working through that book TLA+‘s idiosyncrasy feels like an own goal. There’s this whole comment section song and dance, for compatibility etc… but does anyone actually use something that isn’t the TLA+ toolkit? Why cause yourself pain like that in a vertically integrated system where you are the spec author and the implementation author. I am sure there are reasons, and that is not a reason to not use TLA+. I wonder what the rationale there is.
One ask I have to deepen my TLA+ knowledge is for some more open-ended exercises. Reading along a specification of a model and a problem means that I don’t actually have the opportunity to practice modeling (which is super important to practice). Of course this is a free resource, and the book itself has a lot of ground to cover in relatively little pages. But yeah, give me some relatively nicely packaged problems to work on from my end!
Ah, great! I think I will finally give this a whirl this weekend.
Minor typo in the “Running Models” section of the Setup page: the invariant name you enter in the dialog box should be NoOverdrafts rather than No Overdrafts.
In case it helps other M1 Mac users, there is no native ARM binary of the TLA+ Toolbox, but the x86 version works under Rosetta. And to save someone else the half hour I just spent trying and failing to build an ARM version: it depends on some old versions of Eclipse GUI libraries that don’t have ARM support, as far as I can tell.
I’m excited to dive in! Thanks for all the hard work @hwayne, it’s been apparent just how much of a pure grind this has been. I’m happy you got it done, congratulations! Now for digging into TLA+ :)
I absolutely feel like I understand software at a deeper level after investing time in learning TLA+. That alone is worth it for me personally, but I don’t use it directly at work. What I can tell you I have started to use directly at work is the concept of invariants, and you can do a close approximation of the invariant checking that TLA+ espouses with property-based testing.
TLA+ is still way more powerful, because the model checker can do exhaustive checking whereas property-based testing inputs are random. Unfortunately the main barrier to greater adoption I think is the verification gap - the idea that your TLA+ spec is decoupled from your actual code implementation. There are some really cool solutions being explored to this problem, but there is no one standard solution just yet.
A while back, you said that if I wanted I wanted to learn a formal specification language, and were to pick just one, you’d recommend Alloy. Does that recommendation still hold? And if so, what materials do you recommend for doing so?
I’d have to think on this more. I will think the core ideas of alloy are easier, but it’s harder to apply to many interesting problems, and there’s currently nothing out there that teaches the new logic operators.
I have actually been going through Practical TLA+ and enjoying it, though honestly sometimes it’s a bit hard to go from “I know that this business problem should be modelable” to “here is a sensible model for the problem”.
I know that it’s not actually super important but just working through that book TLA+‘s idiosyncrasy feels like an own goal. There’s this whole comment section song and dance, for compatibility etc… but does anyone actually use something that isn’t the TLA+ toolkit? Why cause yourself pain like that in a vertically integrated system where you are the spec author and the implementation author. I am sure there are reasons, and that is not a reason to not use TLA+. I wonder what the rationale there is.
One ask I have to deepen my TLA+ knowledge is for some more open-ended exercises. Reading along a specification of a model and a problem means that I don’t actually have the opportunity to practice modeling (which is super important to practice). Of course this is a free resource, and the book itself has a lot of ground to cover in relatively little pages. But yeah, give me some relatively nicely packaged problems to work on from my end!
Ah, great! I think I will finally give this a whirl this weekend.
Minor typo in the “Running Models” section of the Setup page: the invariant name you enter in the dialog box should be
NoOverdraftsrather thanNo Overdrafts.In case it helps other M1 Mac users, there is no native ARM binary of the TLA+ Toolbox, but the x86 version works under Rosetta. And to save someone else the half hour I just spent trying and failing to build an ARM version: it depends on some old versions of Eclipse GUI libraries that don’t have ARM support, as far as I can tell.
I’m excited to dive in! Thanks for all the hard work @hwayne, it’s been apparent just how much of a pure grind this has been. I’m happy you got it done, congratulations! Now for digging into TLA+ :)
This looks awesome! Thanks and congrats, Hillel!
Is learning TLA+ useful for everyone / anyone? Is there an ideal role where the knowledge is most applicable?
Anyone feel like they ‘understood’ systems better after taking the course?
There’s a
<plug>run workshops</plug>tag on learntla.com, is that intentionally not a link at the moment?I absolutely feel like I understand software at a deeper level after investing time in learning TLA+. That alone is worth it for me personally, but I don’t use it directly at work. What I can tell you I have started to use directly at work is the concept of invariants, and you can do a close approximation of the invariant checking that TLA+ espouses with property-based testing.
TLA+ is still way more powerful, because the model checker can do exhaustive checking whereas property-based testing inputs are random. Unfortunately the main barrier to greater adoption I think is the verification gap - the idea that your TLA+ spec is decoupled from your actual code implementation. There are some really cool solutions being explored to this problem, but there is no one standard solution just yet.
The “professional TLA+ consultant” is also a link to the workshops! Maybe I should make it a mailto tho
A while back, you said that if I wanted I wanted to learn a formal specification language, and were to pick just one, you’d recommend Alloy. Does that recommendation still hold? And if so, what materials do you recommend for doing so?
I’d have to think on this more. I will think the core ideas of alloy are easier, but it’s harder to apply to many interesting problems, and there’s currently nothing out there that teaches the new logic operators.
Found the link: https://lobste.rs/s/g41wko/announcing_alloydocs#c_4ghy8p
Hell yeah LFG!