[marco_salvatori]

At the risk of being too opinionated, PlusCal is a needless and unproductive diversion. The TLA language and source file structure is mostly standard mathematical notation, using ascii characters. Most people will be familiar already with that mathematical notation before any exposure to TLA. And I wouldn't be able to recommend that people learn just another novel representation for something already known. Learning PlusCal to reason about logical propositions strikes me as comparable to learning an XML notation for manipulating formulas in differential calculus. Yes, we are developers; yes, we are used to XML and, still, ... I don't see how it improves upon writing math.

Mathematical notation is a concise, time tested language for enhancing thought. People should use that to their advantage. As an added advantage, unlike PlusCal, facility in the language of propositional logic generalizes widely to other tools used in formal methods, as well as other technical fields.