4 ms·

I'm reading Hillel's book right now and have just finished Chapter 2 (Intro to PlusCal). I really like it. I've had some failed starts in the past with TLA+. A

I'm reading Hillel's book right now and have just finished Chapter 2 (Intro to PlusCal). I really like it. I've had some failed starts in the past with TLA+. A few observations on the book: a. The language is clear. I feel like making progress at a fairly regular pace. The examples so far could be replicated without any issues. I have both my Kindle and cloud reader open when I read. The screenshots are better in the cloud reader. b. I believe it was a great decision to use PlusCal instead of TLA+ itself. One of the issues coming up to speed in the past was grappling with TLA+. PlusCal just makes it easier. c. I hope that I can actually improve the quality of my C++ programs. I'm currently working on some infrastructure software for embedded systems and have implemented a Hierarchical State Machine "framework" in C++ (https://github.com/tinverse/tsm https://github.com/tinverse/tsm). My goal is to add a pub/sub mechanism and create a HSM that can be distributed over a network. Reviews welcome. Since I just came across this book, going forward, I'll be attempting to develop my specs in PlusCal before actually writing code! d. I think other (to be written) promising books/blogs in this category would be something in the flavor of "Specs to Code" for common design issues. With its focus on concurrency and distributed systems, that implementation language could very well be Rust. Any pointers on porting C++ code to Rust? I'm trying to port above mentioned C++ code to Rust. Respond directly if you can. I don't want to turn this into a discussion on Rust.

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 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 ago
    Right. 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 ago
  P.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).

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 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 ago
  Right. 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 ago
P.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).