Thank you Stephan.
I always thought the beauty of TLA+ is its use of math, which results in concise and easy to understand specs that can also be verified. There are no “implementation details” constructs such as loops, artificial stacks to manage (non-TLA) function calls, program counters, etc. PlusCal brings these details back and makes them part of the spec (translated code). If somebody is fine with TLA+ as it is, do they need PlusCal? Is there anything so important that can be expressed in PlusCal but not in TLA+?
Thank you again,
Yuri