Comment by tonyarkles | Hacker News Reader

Comment by tonyarkles | Hacker News Reader

Parent Full thread

Potentially. I’ve dabbled in TLA+ a few times and have had mixed results; one project turned out spectacularly well, one ran into a problem where I really couldn’t figure out how to model the problem, and one was a failure but TLA+ proved that it was impossible to build a reliable system based on the hard requirements (interfacing with hardware from a 3rd party vendor).

I agree with you in the sense that, after the spectacularly good project, it would have been great to run code gen and get a skeleton to fill in.

I disagree with you in the sense that TLA+ as a language forces you to think about the problem you’re modelling from a very different perspective than how you’d actually write it in an OO/FP/whatever language, and in my experience so far, that has been a very powerful thinking tool. TLA+ doesn’t constrain you to thinking about “how would I write this in Java”, but more in a “how should the communication patterns in this system work” way.

> failure but TLA+ proved that it was impossible to build a reliable system based on the hard requirements

That's probably the most useful result TLA+ can give in comparison to not using it.

Understanding that requirements are impossible after 1-2 weeks of modelling is way better that after 6+ months of coding.

One of my favorite war stories was losing a client after we spent two days trying to model their problem and discovered they didn't actually know what they wanted and they decided to just scrap the project and do something else

> more in a “how should the communication patterns in this system work” way.

I guess that’s the point where I see so much overlap with tests. It seems like we’re talking about test inputs and test outputs.

Even with IPC or Distributed systems I often break problems down in a way that makes them testable in a local system with repeatable results. It’s not 100% perfect b/c you can’t account for all failure scenarios.

I do see your point though about constraints of the target language.

Testing one execution is a start but isn't enough in a nondeterministic distributed system. If you need to check that an invariant is held across all possible executions (e.g. node 3 is down and node 4 is suddenly faster than node 5), you could brute force that yourself but TLA+ has it built in.

That's exactly it. A test verifies one potential execution path. A TLA+ model verifies every execution path, in every ordering that those events could happen.

One of the tricky parts I found was figuring out what granularity to use when writing specifications.

Reply on news.ycombinator.com