When I said we were barely going to cover TLA+, I wasn’t kidding.
Temporal Properties are the heart and soul of TLA+. It’s how the language does anything in the first place. Which is why it’s kind of depressing that I’m going to spend almost no time on it. That’s because of PlusCal abstracts away most of it for us. This section explains a little bit of the parts we, as startup folk, might find useful, and assuage my guilt at not covering a pretty major part of the system.