This is a question I lose sleep over. I keep going back and forth on it. Here's my current position:
_In my experience_, PlusCal is easier for the average engineer to start with, because it lets me decouple learning about behaviors, learning temporal logic, and learning basic predicate logic. It's also my experience that for many people, it's easier and faster to learn PlusCal and then TLA+ than to start with TLA+.
But PlusCal adds syntax and has its own quirks and logic. So if you are fine with TLA+, it's unnecessary overhead and can distract from the core ideas. Here's a quick test:
Op(x, y) ==
/\ x > y
/\ \E s \in S:
/\ x' = F(s)
/\ UNCHANGED y
If that makes sense to you, start with TLA+ proper.
I think this is ultimately an empirical question about "the average beginner." The main issue I have with PlusCal (aside from being more complicated in that it has complicated constructs like subroutines and a stack) is that it could confuse people into thinking that specifying (in TLA+/PlusCal) resembles programming because the PlusCal syntax resembles programming. This can lead to confusion down the line. This is why I think it's a question of would you rather be confused now or later? But if someone finds it easier to start with PlusCal, I see no issue with that.
We choose some element s out of the set S, but only if x > y. That element gets fed into a function whose output is the value of x in the next step. y stays unchanged.
_In my experience_, PlusCal is easier for the average engineer to start with, because it lets me decouple learning about behaviors, learning temporal logic, and learning basic predicate logic. It's also my experience that for many people, it's easier and faster to learn PlusCal and then TLA+ than to start with TLA+.
But PlusCal adds syntax and has its own quirks and logic. So if you are fine with TLA+, it's unnecessary overhead and can distract from the core ideas. Here's a quick test:
If that makes sense to you, start with TLA+ proper.