Modeling Redux with TLA+ (opens in new tab)

Sure, formal methods are irrelevant for your standard CRUD application. However, the use case of AWS got me interested in applying TLA+ to this real-time collaboration feature that we have in the application that I develop. It involves multiple clients communicating over WebSockets, locking and unlocking resources, etc... Expressing the algorithm to TLA+ has:

1. vastly improved my understanding of what is going on and what the potential bad scenarios are. Simply taking a step away from the code, model the high-level algorithm and writing down the invariants that should always hold, makes a big difference.

2. identified real bugs that can occur (and probably have).

So yeah, you can't apply formal methods for everything. But I was pleasantly surprised by how easy it is to express a distributed algorithm in TLA+ and start proving statements about it. Somehow TLA+ manages to bridge the gap between engineering and more theoretical computer science.

[0] https://pron.github.io/posts/tlaplus_part1

> The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing would both be too far removed from the high-level spec, and the process of translation would be negligible in the grand scheme of things, so that an automatic translation, if it is able to produce usable code at all, wouldn't really save you any time.

Hm - the examples in the Go compiler project look relatively good though - would it make sense to use something like this for small portions of a system? I understand that modelling and transpiling an entire system is close to impossible, but a more manageable use case may be a collection of business logic algorithms that are subject to frequent change. In that case you would still want to validate each version after a change, and it would save a lot of time to just autogenerate that particular algorithm in implementation code.

Could you also ask a question that completely gives a counter example? Could you think of a question that does help learning TLA+ because you know something about Leslie Lamport? Have it as a fun exercise for 10 minutes, or not, it might stretch your mind a bit since you claim that you can't see the relevance.

Here is why I like to know about authors who found a field:

Knowing the author may give an idea or context about TLA+. While not strictly necessary, it may be interesting background information that people don't know about. I presume that Lamport has one of the most, if not the most authentic reason for why he created TLA+ in the first place. Reading that reason may motivate people more to learn more about TLA+, or demotivate people more -- but for the right reasons!

Furthermore, discussions can be associative: gabuzome gave book recommendations written by Lamport. I didn't know Lamport wrote one (I know very little about Lamport) and since he now recommended it I'm happy to know that the founder of TLA+ also writes books worthy enough of a recommendation. It personally gives me more confidence to read it and take a crack at it.

Here's a recipe I really like: https://www.epicurious.com/expert-advice/how-to-make-granola...