4 ms·

Every time I see some TLA+ related article, I read it and then spend an hour convincing myself that I don't have time to learn it right now, even though I reall

by daenz 8y ago

Every time I see some TLA+ related article, I read it and then spend an hour convincing myself that I don't have time to learn it right now, even though I really want to. That convincing usually comes in the form of showing that the gains are not worth the effort for the software field that I am in. Can someone change my mind on this?

jononor 8y ago
What software field are you in?
- daenz 8y ago
  General, non-critical software systems. My understanding about TLA+ was that it really shines in critical software systems where the result of the system crashing would be catastrophic. The effort involved in modelling the non-critical systems I work on never seems to outweigh the effort of "write a test, fix the bug, re-deploy"
  - nickpsecurity 8y ago
    It's good for temporal errors, like ordering or concurrency. Those are often the hardest bugs to track down with inspection or testing. Model-checkers such as TLA+ can find them fast. Formal specifications themselves have a few benefits. The first is they force you to make everything explicit that's usually a hidden assumption. From there, they might check the consistency of your system. From there, you might analyze them or generate code from the specs. Spotting hidden or ambiguous assumptions plus detecting interface errors were main benefits in industrial projects going back decades. However, you can get a taste of the benefits by combining Design-by-Contract with contract/property/spec-based testing and runtime checks. Design-by-Contract is a lot like asserts. Should be easy to learn with more obvious value. I'll also note that tools such as Frama-C and SPARK Ada used with code proving are adding or did add the ability to turn all the specs/contracts into runtime checks. So, that's already available in open source or commercial form. And anything you can't spec, just write tests for. :) 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/contracts/ https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
  - hwayne 8y ago
    I'm obviously biased in favor of TLA+, and think it's more useful than people think. But it could also be that another FM might be more useful to you, or that they're not useful at all in your case! Feel free to send me a ping if you want to talk more on this- my email's in the OP link.
  - rtpg 8y ago
    This sort of stuff is maybe not useful in most simple systems and issues, one where "write test, fix bug, re-deploy" feels right. But when you have tighter coupling and a lot more business rules, this stuff becomes useful. For example, imagine that you are writing a billing system. Beyond just the code, there's a design that expects a passing of time and an ordering of operations (user signs up to the system, after a bit they will get invoiced, the amount invoiced will be right, perhaps there's pro-rating) In models where there are a lot of moving parts and where you _don't_ really have locality of code, then this stuff becomes more useful. If you've ever had a bug that exposes an issue not just with the code, but with the entire system and set of assumptions it's built on, it's possible that something like TLA+ could help you a lot for that system
  - jononor 8y ago
    Do you have systems with concurrency and non-trivial resource sharing? That is where TLA+ seems very useful, to use at the design stage.
01100011 8y ago
I love the concept of formal verification, but translating my algorithms into yet another DSL and hoping I get that right seems like a waste of time. I'd rather simulate the algorithm with my brain.
- varelaz 8y ago
  Good luck with this. I heard about practical TLA usage. There was hang up in python asyncio library related to concurrency and it required 24 steps to reproduce. It was found and fixed with TLA help.
  - michael_j_ward 8y ago
    Do you have a source for that? I tried a few google searches and came up empty
    - varelaz 8y ago
      It was part of the talk in PyCon Ukraine 2018, which I took part. https://pyvideo.org/pycon-ukraine-2018/verification-of-concurrent-and-distributed-systems.html https://pyvideo.org/pycon-ukraine-2018/verification-of-concu... That's the video Sorry it's on Russian and amount of steps was 33. Check 28:30
- deleted 8y ago
  [deleted]
blub 8y ago
It's almost certainly not worth the effort, given what you said about your work domain. From what I've seen, TLA is finding a niche for modeling complex concurrent/distributed algorithms. I'd recommend design by contract as a lighter way of verification. And if you don't like the TLA syntax, you could try a verification tool similar to TLA called SPIN, since it kind of looks like C. The reference for SPIN is the book written by the tool's author.
eeZah7Ux 8y ago
In many fields the gains are not worth the effort if you think of validating entire specs or real codebases. Yet TLA+ can be beneficial to validate multiple-step interactions between components e.g. a quorum protocol on a network or locking and messaging between threads. Anything that involves more than one agent and a state machine essentially.

by daenz 8y ago

jononor 8y ago

What software field are you in?

daenz 8y ago
General, non-critical software systems. My understanding about TLA+ was that it really shines in critical software systems where the result of the system crashing would be catastrophic. The effort involved in modelling the non-critical systems I work on never seems to outweigh the effort of "write a test, fix the bug, re-deploy"
- nickpsecurity 8y ago
  It's good for temporal errors, like ordering or concurrency. Those are often the hardest bugs to track down with inspection or testing. Model-checkers such as TLA+ can find them fast. Formal specifications themselves have a few benefits. The first is they force you to make everything explicit that's usually a hidden assumption. From there, they might check the consistency of your system. From there, you might analyze them or generate code from the specs. Spotting hidden or ambiguous assumptions plus detecting interface errors were main benefits in industrial projects going back decades. However, you can get a taste of the benefits by combining Design-by-Contract with contract/property/spec-based testing and runtime checks. Design-by-Contract is a lot like asserts. Should be easy to learn with more obvious value. I'll also note that tools such as Frama-C and SPARK Ada used with code proving are adding or did add the ability to turn all the specs/contracts into runtime checks. So, that's already available in open source or commercial form. And anything you can't spec, just write tests for. :) 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/contracts/ https://hillelwayne.com/post/contracts/ https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
- hwayne 8y ago
  I'm obviously biased in favor of TLA+, and think it's more useful than people think. But it could also be that another FM might be more useful to you, or that they're not useful at all in your case! Feel free to send me a ping if you want to talk more on this- my email's in the OP link.
- rtpg 8y ago
  This sort of stuff is maybe not useful in most simple systems and issues, one where "write test, fix bug, re-deploy" feels right. But when you have tighter coupling and a lot more business rules, this stuff becomes useful. For example, imagine that you are writing a billing system. Beyond just the code, there's a design that expects a passing of time and an ordering of operations (user signs up to the system, after a bit they will get invoiced, the amount invoiced will be right, perhaps there's pro-rating) In models where there are a lot of moving parts and where you _don't_ really have locality of code, then this stuff becomes more useful. If you've ever had a bug that exposes an issue not just with the code, but with the entire system and set of assumptions it's built on, it's possible that something like TLA+ could help you a lot for that system
- jononor 8y ago
  Do you have systems with concurrency and non-trivial resource sharing? That is where TLA+ seems very useful, to use at the design stage.

01100011 8y ago

I love the concept of formal verification, but translating my algorithms into yet another DSL and hoping I get that right seems like a waste of time. I'd rather simulate the algorithm with my brain.

varelaz 8y ago
Good luck with this. I heard about practical TLA usage. There was hang up in python asyncio library related to concurrency and it required 24 steps to reproduce. It was found and fixed with TLA help.
- michael_j_ward 8y ago
  Do you have a source for that? I tried a few google searches and came up empty
  - varelaz 8y ago
    It was part of the talk in PyCon Ukraine 2018, which I took part. https://pyvideo.org/pycon-ukraine-2018/verification-of-concurrent-and-distributed-systems.html https://pyvideo.org/pycon-ukraine-2018/verification-of-concu... That's the video Sorry it's on Russian and amount of steps was 33. Check 28:30
deleted 8y ago
[deleted]

blub 8y ago

It's almost certainly not worth the effort, given what you said about your work domain. From what I've seen, TLA is finding a niche for modeling complex concurrent/distributed algorithms. I'd recommend design by contract as a lighter way of verification. And if you don't like the TLA syntax, you could try a verification tool similar to TLA called SPIN, since it kind of looks like C. The reference for SPIN is the book written by the tool's author.

eeZah7Ux 8y ago

In many fields the gains are not worth the effort if you think of validating entire specs or real codebases. Yet TLA+ can be beneficial to validate multiple-step interactions between components e.g. a quorum protocol on a network or locking and messaging between threads. Anything that involves more than one agent and a state machine essentially.