Nah, different things click with different people. In my experience more beginners find PlusCal easier to start with than "raw" TLA+, which is why I focus on pr

Nah, different things click with different people. In my experience more beginners find PlusCal easier to start with than "raw" TLA+, which is why I focus on presenting it first. But plenty of people find raw TLA+ more natural to start with. Use whatever works best for you- once you have one, learning the other is really fast. What matters much more is getting your foot in the door, y'know? Personally, if I'm not writing teaching or workshop materials, I write specs in raw TLA+. Some of that is due to fixable limitations in PlusCal, but a lot is because it's fundamentally a really elegant way of expressing specifications.