My goodness - i just had an idea for a blog post about modeling real-world processes with TLA+. I had a couple of situations at work recently that weren’t code related that I immediately mapped to a TLA+-like model in my head, and that made me understand them better.
It turns out state machines very naturally model a lot of business processes too. I guess that’s not surprising, seeing as with programming we’re also just modeling business processes, but it’s been surprising for me to be thinking about TLA+ outside of a verification context.
Incidentally the monthly TLA+ community meeting is happening in 1h15m (11 am ET, 8 am PT) today if anybody would like to join! The Teams link is in the schedule you can see here.
Here is the google group post about it. Mostly it takes the form of people talking about what TLA+ stuff they’ve been working on (either development using TLA+ or on the tools themselves), current status of the foundation, stuff like that.
My goodness - i just had an idea for a blog post about modeling real-world processes with TLA+. I had a couple of situations at work recently that weren’t code related that I immediately mapped to a TLA+-like model in my head, and that made me understand them better.
It turns out state machines very naturally model a lot of business processes too. I guess that’s not surprising, seeing as with programming we’re also just modeling business processes, but it’s been surprising for me to be thinking about TLA+ outside of a verification context.
Hah, that’s Leslie Lamport’s open-secret mission: he wants to change how software engineers think using TLA+ as a sort of Trojan Horse!
The universe is a simulation - described in TLA+.
Yeah, TLA+ was primarily created as a notation for thinking, the model checker can’t even check all the things you can write.
Love the Discworld references :)
Incidentally the monthly TLA+ community meeting is happening in 1h15m (11 am ET, 8 am PT) today if anybody would like to join! The Teams link is in the schedule you can see here.
Any links to read about this group that isn’t just a calendar? (Since the calendar doesn’t seem to have any other background info.)
Here is the google group post about it. Mostly it takes the form of people talking about what TLA+ stuff they’ve been working on (either development using TLA+ or on the tools themselves), current status of the foundation, stuff like that.
Happening now!