[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] I've been working on a TLA+ guide


On 08.02.2017 01:28, Hillel Wayne wrote:
> For the past few months I've been working on a TLA+ Guide 
> (www.learntla.com). It's aimed at a less rigorous audience than Specifying 
> Systems or the Hyperbook are: it's a lot less comprehensive and in-depth 
> and focuses more on patterns and troubleshooting. The hope is that it'll be 
> useful for software developers who may not necessarily need the full power 
> of TLA+ but would benefit from having something more sophisticated than 
> unit tests.
> It's still in early drafts but I would love to get some feedback. Feel free 
> to check it out! And please let me know if something is confusing, 
> explained poorly, or flat-out wrong. Writing v1 is the *easy* part, after 
> all. ;)
> Hillel
> PS: While I think it's ready to share with you folks, it's definitely not 
> ready to fully publicize, and I plan on doing five or six more rounds of 
> editing to get it there. Doesn't even have exercises yet.

I really like the approach you've taken in the guide, starting with
PlusCal. As a TLA+ user, it would have saved me many days if something
like this were available when I first started learning TLA+. I think
this will be a very valuable guide for newcomers because it covers the
essentials to get started quickly, and it does so well. Good work! :-)