[pron]

I have mixed feelings about PlusCal. I, too, prefer TLA+ (except for low-level concurrent algorithms, or maybe algorithms best specified with long series of sequential steps), but for many programmers PlusCal can feel more familiar (which may be misleading; specification is not programming, and when you specify in TLA+ it also looks different from programming, but PlusCal looks a lot like programming, but it isn't). I think that those who are not threatened by mathematical notation should start with TLA+, and those who are should start with PlusCal. But there is value in the examples of specifications of the book regardless of the notation used. The central principles of specification are always the same.

[hwayne]

One of these days I gotta write an in-depth discussion of my teaching logic. The reasons I have for starting with PlusCal are fairly complex, and there are also disadvantages to it, too. But I still think that for many engineers, it's easier to learn PlusCal and then TLA+ than to go straight to TLA+.

[tonyarkles]

Lamport agrees with that as well, from what I recall going through his videos. PlusCal for most engineers, TLA+ for people who like to think in math.

And just another Thank You. Your material helped me on my journey too, even though I ended up favouring TLA+ personally.