Hacker News Reader

Comment by djb_hackernews | Hacker News Reader

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it.

Do you know of any straight forward non-trivial examples? Something a little more complex than "hello world" and something that isn't abstract?

View on HN

There's a few I can think of! First, the TLA+ GitHub repo has a bunch of examples[0]. The best one to start with is the Die Hard puzzle[1], where the heroes must obtain four gallons of water given only three and five gallon jugs. In the spec[2] we set up the system and specify all possible actions; then we model-check the system to see whether it can spit out an execution trace of actions to reach a state where we have four gallons of water in a jug.

The Wikipedia article also has some good example specs[3].

For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep.

[0] https://github.com/tlaplus/Examples/tree/master/specificatio...

[1] https://www.youtube.com/watch?v=6cAbgAaEOVE

[2] https://github.com/tlaplus/Examples/blob/master/specificatio...

[3]https://en.wikipedia.org/wiki/TLA+

I wrote an essay[0] about a non-trivial example I did at my company. We had to work with several finicky APIs and the TLA+ spec caught several critical bugs with it. Plus, it's purely a business logic system, so it's pretty concrete.

If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises.

[0] https://medium.com/espark-engineering-blog/formal-methods-in...

[1] https://learntla.com/introduction/

Following your introduction now, it is a great quick-start tutorial, thanks for creating it.

I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified?

SAM can also be used for stateful API/Microservice orchestrations [2]

If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation) I gave this lecture last month [3].

[1] http://sam.js.org

[2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api...

[3] http://cloudsentinel.com/sam-state-machines-and-computation....

You wonder if there are code generation possibilities...

Actually, TLA+ (again the way I understand it), after nearly 20 years of MDSE, convinced me that I would very rarely need to generate code. It's a much better value proposition to write correctly factored code. TLA+ is one of the most amazing element of Computer Science. Everyone who writes code should have at least a basic understanding of it.

As someone who worked with distributed systems for many years before using TLA+ to find bugs and validate work: It's possible to understand it.

I think it would help to have a good mentor, as I did, or a lecture series from the language inventor. I ran through the trial version of these videos when Lamport was developing them and it's quite approachable even for someone who's more of a liberal arts kind of person.

I work on distributed systems and have started pushing for us to use TLA+/PlusCal to model them. I have a simple PlusCal model of a system with two threads which juggles network and disk I/O which I can e-mail you if you like. It's not at all a complex system, but I think it captures the basics of modeling concurrency and I/O well.

Reply on news.ycombinator.com