3 ms·
> One of the issues coming up to speed in the past was grappling with TLA+. PlusCal just makes it easier. I think this has both pros and cons. PlusCal, being e
by pron 8y ago
> One of the issues coming up to speed in the past was grappling with TLA+. PlusCal just makes it easier.
I think this has both pros and cons. PlusCal, being essentially a formal pseudo-code, is much more familiar to programmers than TLA+, and familiarity can greatly assist learning. The downside is that TLA+ is much simpler -- though far less familiar -- than PlusCal (or any programming or programming-like formalism), as it shares the complexities of code (although programmers are used to ignoring them), and at some point if you work with PlusCal you will have to learn and understand it and go through the necessary process of "unlearning" code and thinking in simpler terms. Some may find it easier to start with that and see why any code is more complicated than you may think; after that, learning PlusCal comes for free once you see the translation to TLA+.
Personally, I find writing specifications in PlusCal less convenient and less clear than writing them in TLA+, unless you must reason at the code level (like in the case of low-level concurrent algorithms, where interleaving of particular instructions is crucial). PlusCal, however, has the advantage of being more communicable to those unfamiliar with TLA+, as it reads like pseudo-code.
> something in the flavor of "Specs to Code"
If a programmer can turn an informal specification (or even a set of requirements to code) then transforming formal ones, which are more precise, shouldn't be an issue. But on a theoretical level, once you become more comfortable and experienced with TLA+ you'll see that the notion of specs to code is a special case of a very general and powerful concept called refinement, which forms the very core of TLA -- the Temporal Logic of Actions -- the logic at the heart of TLA+. In fact, in TLA, the ordinary logical expression A ⇒ B, i.e. A implies B, means A refines or implements B (and conversely, B abstracts A).
- pwnna 8y agoI 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.)
- pron 8y agoP.S. I think that learning TLA+ is easier (and takes less time) than learning Python on Javascript provided you can forget everything you know about programming, or, harder still, remember that despite superficial similarities, TLA+ is not programming (confusing a TLA+ operator with a subroutine or thinking about things like evaluation order are bound to bite you sooner or later). This is, I think, the hardest part about learning TLA+ (at least, it was the hardest part for me).