1. 30
    1. 6

      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.

      1. 3

        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!

        1. 2

          The universe is a simulation - described in TLA+.

      2. 1

        Yeah, TLA+ was primarily created as a notation for thinking, the model checker can’t even check all the things you can write.

    2. 3

      Love the Discworld references :)

    3. 2

      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.

      1. 1

        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.)

        1. 2

          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.

          1. 1

            Happening now!