Hacker News Reader

Comment by bluejekyll | Hacker News Reader

Preface, I don’t know TLA+ or Coq, but I get the impression from examples, that it is strongly reminiscent of test-driven-development.

I can see the advantage, but I wonder if there’s potential for writing the proofs in the target language, verifying the logic, then building the code, and verifying the code meets the proofs.

Is this something anyone is looking into? I could imagine a macro in Rust for example that is TLA+, that takes standard test input, verifies the logic, then you feed in the real implementations.

View on HN

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.

The claim I read is that formal methods aren't tractable past X LoC (IIRC it was in the thousands). So you can directly verify a small application/module, or you can verify the high-level design of a larger thing, then write code to that spec. Can't find the source anymore though.

>strongly reminiscent of test-driven-development

Tests only cover the cases you think of. Proof systems let you validate claims about all possible executions.

Reply on news.ycombinator.com