Hacker News Reader

I’ve used TLA+ to model a deployment pipeline. It helped to demonstrate the safety property we needed that process to maintain.

The code running the deploy process is messy and complex. But the a spec doesn’t have to be. You can represent as much or as little detail as you need.

View on HN

Cool! And you make a good point: just because the actual software has 100 corner cases, doesn't mean the model has to. It can still be useful even if it just models an interesting part of the problem.

How do you know whether your TLA+ model is accurate?

With one client I have, we know the TLA+ model is accurate because we're extracting tests directly from the spec. It's kind of a riff on what MongoDB does in this paper: https://arxiv.org/abs/2006.00915

Reply on news.ycombinator.com