5 ms·

I'd love to read about that in detail. Are there any publicly available documents you could share?

by Leace 8y ago

tluyben2 8y ago
I am hoping to find the time to write something, preferably a (free) book; I think I might find the time this summer for that.
- Tomte 8y ago
  When you decide to start, collect mail adresses of interested readers. Don't just assume people will stumble upon your book, seek out readers long before the book is finished. I recently told this on Twitter to an Academic who had just finished writing a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. She had never thought about collecting people's mail addresses, even though dozens (if not hundreds) of people replied on Twitter that they'd be interested in reading the book.
  - detaro 8y ago
    > a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. Sounds interesting, link?
    - Tomte 8y ago
      Erm, not Middle Ages, Rennaissance, of course! https://www.amazon.de/Venices-Secret-Service-Intelligence-Renaissance/dp/0198791313 https://www.amazon.de/Venices-Secret-Service-Intelligence-Re...
Ixiaus 8y ago
Hillel Wayne[1] has written a bunch about TLA+ for lay programmers like me. I've found his blog posts pretty good, I also bought his book Practical TLA+ which I like. He also wrote the free web book Learn TLA+[2]. [1]: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ [2]: https://learntla.com/introduction/ https://learntla.com/introduction/
- lintuxvi 8y ago
  He also runs workshops for teams wanting to incorporate this into their toolset.
Twirrim 8y ago
Anecdotally, the team I was in in AWS needed to build a complicated component, one that, should it get it wrong, would be disastrous for the service. They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production. They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task. It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear. Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code. In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.
- baq 8y ago
  Lamport claims on his website that Amazon uses TLA+ and has used it for quite a while now. Saying that to confirm plausibility of this story.
  - Tomte 8y ago
    https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
  - Twirrim 8y ago
    Amazon/AWS has published a few white papers about their use of TLA+ and other Formal Methods:http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p.... James Hamilton is a fan of TLA+, and talks about its use in Amazon: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
- 8y ago

I'd love to read about that in detail. Are there any publicly available documents you could share?

by Leace 8y ago

I'd love to read about that in detail. Are there any publicly available documents you could share?

I am hoping to find the time to write something, preferably a (free) book; I think I might find the time this summer for that.

Tomte 8y ago
When you decide to start, collect mail adresses of interested readers. Don't just assume people will stumble upon your book, seek out readers long before the book is finished. I recently told this on Twitter to an Academic who had just finished writing a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. She had never thought about collecting people's mail addresses, even though dozens (if not hundreds) of people replied on Twitter that they'd be interested in reading the book.
- detaro 8y ago
  > a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. Sounds interesting, link?
  - Tomte 8y ago
    Erm, not Middle Ages, Rennaissance, of course! https://www.amazon.de/Venices-Secret-Service-Intelligence-Renaissance/dp/0198791313 https://www.amazon.de/Venices-Secret-Service-Intelligence-Re...

Ixiaus 8y ago

Hillel Wayne[1] has written a bunch about TLA+ for lay programmers like me. I've found his blog posts pretty good, I also bought his book Practical TLA+ which I like. He also wrote the free web book Learn TLA+[2]. [1]: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ [2]: https://learntla.com/introduction/ https://learntla.com/introduction/

lintuxvi 8y ago
He also runs workshops for teams wanting to incorporate this into their toolset.

Twirrim 8y ago

Anecdotally, the team I was in in AWS needed to build a complicated component, one that, should it get it wrong, would be disastrous for the service. They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production. They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task. It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear. Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code. In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.

baq 8y ago
Lamport claims on his website that Amazon uses TLA+ and has used it for quite a while now. Saying that to confirm plausibility of this story.
- Tomte 8y ago
  https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
- Twirrim 8y ago
  Amazon/AWS has published a few white papers about their use of TLA+ and other Formal Methods:http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p.... James Hamilton is a fan of TLA+, and talks about its use in Amazon: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
8y ago