3 ms·
I think the key bottleneck for formal methods in "normal" software is that formal methods imply a formal model that you're checking against -- and most software
by Taikonerd 1y ago
I think the key bottleneck for formal methods in "normal" software is that formal methods imply a formal model that you're checking against -- and most software doesn't have that.
For example, deployment software. There's probably some way to formally model deployment. But most deployment software in the wild is written like, "here are 100 things that can go wrong while you're deploying, and 100 corresponding business rules for what to do."
I do sometimes fantasize about a more pure-Computer-Science world where all text formats are a formally-defined grammar, all systems are state machines, and everything has a spec ;-)
- agentultra 1y agoI’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.
- gooosle 1y agoHow do you know whether your TLA+ model is accurate?
- hwayne 1y agoWith 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 https://arxiv.org/abs/2006.00915
- Taikonerd 1y agoCool! 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.