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.