4 ms·
Can someone who has learned TLA+ comment on how useful it is has been for you?
by dqpb 8y ago
Can someone who has learned TLA+ comment on how useful it is has been for you?
- mavelikara 8y agoSomeone from AWS posted this few days ago: https://news.ycombinator.com/item?id=19634915 https://news.ycombinator.com/item?id=19634915
- k__ 8y agoIs this somehow integrated with Java or does it work with a programming language of my choice?
- strangecasts 8y agoSpecifications aren't tied to any specific programming language - you're outlining how the algorithm should work, not the implementation. (You can write Java code and invoke it during model-checking if you really need to, but I haven't come across any situation where it's actually necessary.)
- k__ 8y agoAh, okay. I had the impression it was about somehow writing a program in a more strict language and then exporting it to Java. I don't do much algorithmic design.
- hwayne 8y agoI've written specifications of Ruby and Python codebases before, and worked with people who wrote Java, C, and Haskell code. It's pretty versatile!
- raegis 8y agoI spent a 6 month parental leave learning it and experimenting with it. I enjoyed writing specifications so much that I thought programming was a waste of time. You should watch the video lectures. The first 2 or 3 will get you going. A first simple exercise might be to specify the least common multiple following Lamport's GCD example. I'm a math major, by the way.
- endiangroup 8y agoIt uncovered an oversight in an algorithm we put together for managing distributed sessions. An invariant showed that our algorithm would accept and consider valid tokens that were ahead of the 'master' counter, which theoretically shouldn't of been a possible input in practice but now that we know we've added an additional guard. Original comment: https://news.ycombinator.com/item?id=19662123 https://news.ycombinator.com/item?id=19662123