3 ms·
I find that learning raw TLA+ to the point where you're comfortable reading it and internalizing what the spec is saying to be a critical skill to be able to wr
by pwnna 8y ago
I find that learning raw TLA+ to the point where you're comfortable reading it and internalizing what the spec is saying to be a critical skill to be able to write specifications successfully. This is because PlusCal translates directly to TLA+, which means that:
1. To debug errors given to me by TLC, I generally find that it's easier to look at the TLA+ spec directly.
2. It is sometimes easier to see what your algorithm is doing directly in TLA+. I find that I will write the algo in PlusCal, it gets translated, and I can get a better understanding of how the system works by looking at the TLA+ spec. Example: the "process model" of PlusCal does hide some of the ideas. Multiple process are just P1 \/ P2 \/ P3 ....,
3. There are some oddities within PlusCal (label placement, the with statements) that makes much more sense if you understand the TLA+ foundation.
What I really wish is that I can write partly PlusCal and partly TLA+ for maximum flexibility. However, it's kinda ackward to do within the current framework.
- pron 8y agoRight. In addition, you miss out on the notion of refinement (ordinary implication in TLA+) which is the most powerful (and most foundational) idea of the formalism. But I think many developers may be threatened by the unfamiliarity of TLA+, and PlusCal serves as a gateway drug, as it's often useful enough on its own (you're right that you need to know at least a bit of TLA+ to understand some of the tooling's output). If "PlusCal first" makes TLA+ less threatening and hopefully more approachable to many developers, then the approach is doing its job. (BTW, I wouldn't call it "raw TLA+" as "raw TLA" is a particular logic that Lamport uses to introduce TLA, so the term may be confusing.)