Modeling Message Queues in TLA+
I&#x27;m reading Hillel&#x27;s book right now and have just finished Chapter 2 (Intro to PlusCal). I really like it. I&#x27;ve had some failed starts in the past with TLA+. A few observations on the book:<p>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.<p>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.<p>c. I hope that I can actually improve the quality of my C++ programs. I&#x27;m currently working on some infrastructure software for embedded systems and have implemented a Hierarchical State Machine &quot;framework&quot; in C++ (<a href="https:&#x2F;&#x2F;github.com&#x2F;tinverse&#x2F;tsm" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;tinverse&#x2F;tsm</a>). My goal is to add a pub&#x2F;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&#x27;ll be attempting to develop my specs in PlusCal before actually writing code!<p>d. I think other (to be written) promising books&#x2F;blogs in this category would be something in the flavor of &quot;Specs to Code&quot;  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&#x27;m trying to port above mentioned C++ code to Rust. Respond directly if you can. I don&#x27;t want to turn this into a discussion on Rust.