4 ms·
Honestly... Just like with writing extensive unit tests, you will then end up basically writing the program twice. Which is not going to appeal to the "move as
by cmrdporcupine 1y ago
Honestly... Just like with writing extensive unit tests, you will then end up basically writing the program twice. Which is not going to appeal to the "move as fast as possible" crowd.
- pjmlp 1y agoAt least the unit tests can validate the actual implementation.
- cmrdporcupine 1y agoI mean you only validate the parts that the test writer thought to verify. It will always remain unexhaustive and full of holes.
- pjmlp 1y agoWhich still remains more than what the TLA+ theoric model can offer.
- stusmall 1y agoThis comment thread is on an article about how Mongo applies TLA+ models to an implementation. They talk about how they use the model to generate test cases for the application. There are fair criticisms of formal modeling, but that they can't test the implementation isn't one. I mention in another comment, I ended up not going the TLA+ route. It isn't because it cannot offer this, it's because it's a heavy, opinionated investment. That is a good trade off for some systems, like databases, but not for everything.
- pjmlp 1y agoThe criticism is regarding TLA+ in particular, versus other formal verification tools that generate code directly from the model without additional effort building tools, or manual verification that model and actual code map to the same semantics.