7 ms·

Modeling Redux with TLA+

132 points by hellerve 9y ago

mettamage 9y ago
Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don't know about any of this, I invite you to take a look. Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2]. 1. https://en.wikipedia.org/wiki/Leslie_Lamport https://en.wikipedia.org/wiki/Leslie_Lamport 2. https://www.distributed-systems.net/index.php/books/distributed-systems-3rd-edition-2017/ https://www.distributed-systems.net/index.php/books/distribu...
- raister 9y ago
  I don't see the relevance on knowing Leslie Lamport to learn about TLA+ - what is the matter? One thing has nothing to do with the other... Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?
  - mettamage 9y ago
    "Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?" Of course not. That question is too simple, and you know it! ;) 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.
    - sseveran 9y ago
      Plus his website has a bunch of good resources linked from it. http://www.lamport.org http://www.lamport.org
  - andrewflnr 9y ago
    Affect my decision to learn TLA? Probably not. Entertaining? Interesting? Something I would want to know? Yes.
- gabuzome 9y ago
  Yes Lamport started and maintains TLA+. I found his hyperbook to be a good introduction to TLA+ and PlusCal. http://lamport.azurewebsites.net/tla/hyperbook.html http://lamport.azurewebsites.net/tla/hyperbook.html
fouc 9y ago
> TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint. Very cool.
- raister 9y ago
  Cool and impossible to apply to real world projects due to budget or deadlines.
  - RubenSandwich 9y ago
    People said the same things about unit and integration tests a decade ago.
    - lou1306 9y ago
      And about optimizing compilers, neural networks, and static program analysis four decades ago. Computer science is a fast-moving field, sure. But not all of today's research bring tangible results by the end of the week, and we should be comfortable with that.
      - RubenSandwich 9y ago
        I generally agree, but formal methods I can say with confidence will get adopted in the future. Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on the bug-free/security question is this: "We wrote it according to X standard and wrote tests to cover those cases.". Formal methods allow us to prove a system is bug-free/secure. It is the evolution of testing. I do not know how far off it is, but because we have already adopted testing I believe formal methods will get adopted as well.
        9y ago
nickpsecurity 9y ago
His main site he mentions at the end is learntla.com. That's a good tutorial for using a subset of it that will get stuff done without trying to read a bunch of books on heavier stuff. He and I both also recommend Alloy for a taste in formal methods or blueprints like fouc said since it's designed for beginners with good guides and tutorials. TLA+/PlusCal with its model-checker is better at modeling order of execution (esp concurrency/distributed) whereas Alloy's is focused on structure of your program. Finally, Design-by-Contract combined with property-based testing or AFL-style testing with properties/contracts as runtime checks is probably combo most applicable to most programming languages and situations. If you know conditionals, you can use DbC in a lots of situations. http://alloytools.org http://alloytools.org https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
ajmurmann 9y ago
Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: https://youtu.be/_9B__0S21y8 https://youtu.be/_9B__0S21y8 If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.
- mpiedrav 9y ago
  It was 7 lb (3.18 kg) of sesame brittle. Indeed, an entertaining and practical talk on TLA+.
  - hwayne 9y ago
    _That said_, I've been making a lot of homemade granola recently. Maybe I should try bringing that next time! Here's a recipe I really like: https://www.epicurious.com/expert-advice/how-to-make-granola-without-a-recipe-article https://www.epicurious.com/expert-advice/how-to-make-granola...
nazri1 9y ago
Any takers for doing this in lisp? ;)
- abhirag 9y ago
  Not formal verification, but you can specify and validate application state of SPAs written in clojurescript using clojure.spec(https://clojure.org/about/spec https://clojure.org/about/spec). Example -- (https://github.com/Day8/re-frame/blob/master/examples/todomvc/src/todomvc/db.cljs https://github.com/Day8/re-frame/blob/master/examples/todomv...)
- hwayne 9y ago
  You might wanna check out ACL2, which is a theorem prover rooted in common lisp: http://www.cs.utexas.edu/users/moore/acl2/ http://www.cs.utexas.edu/users/moore/acl2/
elcapitan 9y ago
Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.
- mettamage 9y ago
  There is some discussion on it here about TLA+ itself: https://news.ycombinator.com/item?id=14373359 https://news.ycombinator.com/item?id=14373359 Not about JavaScript though, but C and Java.
  - elcapitan 9y ago
    Thanks, will look into that - I read that Coq can generate Haskell etc, so I was wondering if something similar exists.
- pron 9y ago
  There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. 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. That's not to say that you shouldn't also reasons about more local properties at the code level, and there are good code-level verification tools (advanced ones include Frama-C for C, OpenJML/Krakatoa for Java and SPARK for Ada) just for that. It is possible to use TLA+ (and other tools, like Coq or Isabelle) for what's known as end-to-end verification, which means verifying the important global properties all the way down to the code level (and even machine-code level), but the process is so laborious that it is virtually never worth the effort, and, in fact, it has never been achieved for any but very small programs (and even then at great cost). [1]: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo

132 points by hellerve 9y ago

Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don't know about any of this, I invite you to take a look. Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2]. 1. https://en.wikipedia.org/wiki/Leslie_Lamport https://en.wikipedia.org/wiki/Leslie_Lamport 2. https://www.distributed-systems.net/index.php/books/distributed-systems-3rd-edition-2017/ https://www.distributed-systems.net/index.php/books/distribu...

raister 9y ago
I don't see the relevance on knowing Leslie Lamport to learn about TLA+ - what is the matter? One thing has nothing to do with the other... Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?
- mettamage 9y ago
  "Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?" Of course not. That question is too simple, and you know it! ;) 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.
  - sseveran 9y ago
    Plus his website has a bunch of good resources linked from it. http://www.lamport.org http://www.lamport.org
- andrewflnr 9y ago
  Affect my decision to learn TLA? Probably not. Entertaining? Interesting? Something I would want to know? Yes.
gabuzome 9y ago
Yes Lamport started and maintains TLA+. I found his hyperbook to be a good introduction to TLA+ and PlusCal. http://lamport.azurewebsites.net/tla/hyperbook.html http://lamport.azurewebsites.net/tla/hyperbook.html

fouc 9y ago

> TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint. Very cool.

raister 9y ago
Cool and impossible to apply to real world projects due to budget or deadlines.
- RubenSandwich 9y ago
  People said the same things about unit and integration tests a decade ago.
  - lou1306 9y ago
    And about optimizing compilers, neural networks, and static program analysis four decades ago. Computer science is a fast-moving field, sure. But not all of today's research bring tangible results by the end of the week, and we should be comfortable with that.
    - RubenSandwich 9y ago
      I generally agree, but formal methods I can say with confidence will get adopted in the future. Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on the bug-free/security question is this: "We wrote it according to X standard and wrote tests to cover those cases.". Formal methods allow us to prove a system is bug-free/secure. It is the evolution of testing. I do not know how far off it is, but because we have already adopted testing I believe formal methods will get adopted as well.
      - 9y ago

nickpsecurity 9y ago

His main site he mentions at the end is learntla.com. That's a good tutorial for using a subset of it that will get stuff done without trying to read a bunch of books on heavier stuff. He and I both also recommend Alloy for a taste in formal methods or blueprints like fouc said since it's designed for beginners with good guides and tutorials. TLA+/PlusCal with its model-checker is better at modeling order of execution (esp concurrency/distributed) whereas Alloy's is focused on structure of your program. Finally, Design-by-Contract combined with property-based testing or AFL-style testing with properties/contracts as runtime checks is probably combo most applicable to most programming languages and situations. If you know conditionals, you can use DbC in a lots of situations. http://alloytools.org http://alloytools.org https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/

ajmurmann 9y ago

Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: https://youtu.be/_9B__0S21y8 https://youtu.be/_9B__0S21y8 If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.

mpiedrav 9y ago
It was 7 lb (3.18 kg) of sesame brittle. Indeed, an entertaining and practical talk on TLA+.
- hwayne 9y ago
  _That said_, I've been making a lot of homemade granola recently. Maybe I should try bringing that next time! Here's a recipe I really like: https://www.epicurious.com/expert-advice/how-to-make-granola-without-a-recipe-article https://www.epicurious.com/expert-advice/how-to-make-granola...

nazri1 9y ago

Any takers for doing this in lisp? ;)

abhirag 9y ago
Not formal verification, but you can specify and validate application state of SPAs written in clojurescript using clojure.spec(https://clojure.org/about/spec https://clojure.org/about/spec). Example -- (https://github.com/Day8/re-frame/blob/master/examples/todomvc/src/todomvc/db.cljs https://github.com/Day8/re-frame/blob/master/examples/todomv...)
hwayne 9y ago
You might wanna check out ACL2, which is a theorem prover rooted in common lisp: http://www.cs.utexas.edu/users/moore/acl2/ http://www.cs.utexas.edu/users/moore/acl2/

elcapitan 9y ago

Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.

mettamage 9y ago
There is some discussion on it here about TLA+ itself: https://news.ycombinator.com/item?id=14373359 https://news.ycombinator.com/item?id=14373359 Not about JavaScript though, but C and Java.
- elcapitan 9y ago
  Thanks, will look into that - I read that Coq can generate Haskell etc, so I was wondering if something similar exists.
pron 9y ago
There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. 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. That's not to say that you shouldn't also reasons about more local properties at the code level, and there are good code-level verification tools (advanced ones include Frama-C for C, OpenJML/Krakatoa for Java and SPARK for Ada) just for that. It is possible to use TLA+ (and other tools, like Coq or Isabelle) for what's known as end-to-end verification, which means verifying the important global properties all the way down to the code level (and even machine-code level), but the process is so laborious that it is virtually never worth the effort, and, in fact, it has never been achieved for any but very small programs (and even then at great cost). [1]: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo