Have you looked at PlusCal [1][2]? It's more natural for many software developers and compiles down to TLA+.

[1] https://en.wikipedia.org/wiki/PlusCal

[2] https://lamport.azurewebsites.net/tla/p-manual.pdf

Yes, I did. I prefer math/logic syntax, and I often like to work with pen and paper, and those are my main reasons for preferring TLA+ syntax over PlusCal. The author of Practical TLA+ says PlusCal is innately less expressive.

Even so, pron elsewhere recommends reading Practical TLA+ for other reasons, so I think I'll learn PlusCal anyway. I appreciate the suggestion.

I have mixed feelings about PlusCal. I, too, prefer TLA+ (except for low-level concurrent algorithms, or maybe algorithms best specified with long series of sequential steps), but for many programmers PlusCal can feel more familiar (which may be misleading; specification is not programming, and when you specify in TLA+ it also looks different from programming, but PlusCal looks a lot like programming, but it isn't). I think that those who are not threatened by mathematical notation should start with TLA+, and those who are should start with PlusCal. But there is value in the examples of specifications of the book regardless of the notation used. The central principles of specification are always the same.

One of these days I gotta write an in-depth discussion of my teaching logic. The reasons I have for starting with PlusCal are fairly complex, and there are also disadvantages to it, too. But I still think that for many engineers, it's easier to learn PlusCal and then TLA+ than to go straight to TLA+.

Lamport agrees with that as well, from what I recall going through his videos. PlusCal for most engineers, TLA+ for people who like to think in math.

And just another Thank You. Your material helped me on my journey too, even though I ended up favouring TLA+ personally.

I would recommend exploring Emotional Brain Training (EBT) [1]. Wired for Joy [2] and Spiral Up [3] are two related books on the subject. Find a therapist that works in this space to coach you through it.

[1] https://www.ebtconnect.net/what_is_ebt

[2] https://www.amazon.com/Wired-Joy-Revolutionary-Creating-Happ...

[3] Sorry I can't find it anywhere

A Nickel's Worth's guide on variable naming seems like a relevant read here:

https://a-nickels-worth.blogspot.ie/2016/04/a-guide-to-namin...

I think that's right. Anecdotally as a user of Peach, the four biggest complaints I've had/heard are: 1) late delivery 2) food at wrong temperature when delivered 3) food doesn't taste good 4) people tired of the same menu options repeated too often

Sounds like Peach: https://www.peachd.com/

Except peach serves lunch instead of dinner. They appear to have the restaurants deliver the food themselves. Your office needs to have 50 people who have signed up for the service before they'll start offering menu items in that location.

Thanks for sharing that! Yes the key difference here on the backend is that we make the food ourselves. But you're abs. right that from the frontend it's very similar.

This applies to human DNA only? Plant seeds don't get protection?

What are the hidden fees in the S3 use case?