5 ms·

TLA+ in Practice and Theory, Part 4: Order in TLA+

143 points by hiq 9y ago

couac 9y ago
Cool. I was waiting for it :) Question: would you have examples of TLA+ specs that are not related to distributed algos (raft, paxos, etc.) or puzzles (die hard, etc.)?
- pron 9y ago
  Part 3 has examples of two sorting algorithms. There are also examples in these links: https://learntla.com/models/example/ https://learntla.com/models/example/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.linkedin.com/pulse/lamports-tla-spec-testing-why-youre-using-nira-amit https://www.linkedin.com/pulse/lamports-tla-spec-testing-why... https://github.com/tlaplus/Examples/tree/master/specifications/allocator https://github.com/tlaplus/Examples/tree/master/specificatio... https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/CachingMemory https://github.com/tlaplus/Examples/tree/master/specificatio...
- Jach 9y ago
  This link hit HN not too long ago: https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f https://medium.com/espark-engineering-blog/formal-methods-in... (https://news.ycombinator.com/item?id=14221848 https://news.ycombinator.com/item?id=14221848) (Edit: Ah, already linked within pron's second link... Oh well.)
zukzuk 9y ago
This is thorough and overall really well done, but after reading through Part 1, I can't help but trot out Brian Cantwell Smith's "The Limits of Correctness" https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...
- skybrian 9y ago
  Or as the poet put it, at best we have "imaginary gardens with real toads in them."
- pron 9y ago
  I'm the author of the post, and just last year I wrote a long post about the difficulty -- both theoretical and practical -- of software correctness[1]. People who understand formal methods know this, and treat the task with humility and pragmatism. Nobody's claiming that we can "just" write "correct" software whenever we like with just a few tricks. [1]: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity
skybrian 9y ago
Maybe a simple metaphor for what TLA+ can be used for would be to think of a "game" consisting of a "board" and "moves", and then exploring what game states can be reached? So the question in a specification is deciding what the board looks like, what the legal moves are, and what properties you're interested in. Then model-checking is exploring the game tree to some depth to find out if there are move sequences that will reach interesting states. You wouldn't write a chess or Go-playing program in TLA+, but most discrete systems have smaller trees than that. It seems like it would reasonable to compare this to QuickCheck-style testing or fuzzing, except that it's entirely done in a different language.
- pron 9y ago
  You are talking about model checkers. TLA+ is not a model checker. It is a specification language, like Coq or Isabelle. It's a mathematical language for describing programs. What you do with those descriptions may include using some mechanical tools. The tools for TLA+ include a mechanical proof assistant (like Coq and Isabelle) and it also has a model checker. But you can do more with TLA+ than use the model checker (although the model checker is often the most cost-effective use).
- Normal_gaussian 9y ago
  > Maybe a simple metaphor for what TLA+ can be used for would be to think of a "game" consisting of a "board" and "moves", and then exploring what game states can be reached? Hmm... A "board" with "moves" sounds an awful lot like the first part of a Turing Machine...
hullsean 9y ago
Same science holds for price of wine. The more general truth is quality does not correlate with cost. Google Rory Sutherlands TED talk
- hullsean 9y ago
  Oops wrong post.

143 points by hiq 9y ago

Cool. I was waiting for it :) Question: would you have examples of TLA+ specs that are not related to distributed algos (raft, paxos, etc.) or puzzles (die hard, etc.)?

pron 9y ago
Part 3 has examples of two sorting algorithms. There are also examples in these links: https://learntla.com/models/example/ https://learntla.com/models/example/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.linkedin.com/pulse/lamports-tla-spec-testing-why-youre-using-nira-amit https://www.linkedin.com/pulse/lamports-tla-spec-testing-why... https://github.com/tlaplus/Examples/tree/master/specifications/allocator https://github.com/tlaplus/Examples/tree/master/specificatio... https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/CachingMemory https://github.com/tlaplus/Examples/tree/master/specificatio...
Jach 9y ago
This link hit HN not too long ago: https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f https://medium.com/espark-engineering-blog/formal-methods-in... (https://news.ycombinator.com/item?id=14221848 https://news.ycombinator.com/item?id=14221848) (Edit: Ah, already linked within pron's second link... Oh well.)

zukzuk 9y ago

This is thorough and overall really well done, but after reading through Part 1, I can't help but trot out Brian Cantwell Smith's "The Limits of Correctness" https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...

skybrian 9y ago
Or as the poet put it, at best we have "imaginary gardens with real toads in them."
pron 9y ago
I'm the author of the post, and just last year I wrote a long post about the difficulty -- both theoretical and practical -- of software correctness[1]. People who understand formal methods know this, and treat the task with humility and pragmatism. Nobody's claiming that we can "just" write "correct" software whenever we like with just a few tricks. [1]: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

skybrian 9y ago

Maybe a simple metaphor for what TLA+ can be used for would be to think of a "game" consisting of a "board" and "moves", and then exploring what game states can be reached? So the question in a specification is deciding what the board looks like, what the legal moves are, and what properties you're interested in. Then model-checking is exploring the game tree to some depth to find out if there are move sequences that will reach interesting states. You wouldn't write a chess or Go-playing program in TLA+, but most discrete systems have smaller trees than that. It seems like it would reasonable to compare this to QuickCheck-style testing or fuzzing, except that it's entirely done in a different language.

pron 9y ago
You are talking about model checkers. TLA+ is not a model checker. It is a specification language, like Coq or Isabelle. It's a mathematical language for describing programs. What you do with those descriptions may include using some mechanical tools. The tools for TLA+ include a mechanical proof assistant (like Coq and Isabelle) and it also has a model checker. But you can do more with TLA+ than use the model checker (although the model checker is often the most cost-effective use).
Normal_gaussian 9y ago
> Maybe a simple metaphor for what TLA+ can be used for would be to think of a "game" consisting of a "board" and "moves", and then exploring what game states can be reached? Hmm... A "board" with "moves" sounds an awful lot like the first part of a Turing Machine...

hullsean 9y ago

Same science holds for price of wine. The more general truth is quality does not correlate with cost. Google Rory Sutherlands TED talk

hullsean 9y ago
Oops wrong post.