21 ms·
Hundred percent. All about trade-offs. Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios. TLA
by agentultra 16d ago
Hundred percent. All about trade-offs.
Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios.
TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.
- bunderbunder 16d agoYeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve that problem, but perhaps they can mitigate it.
- agentultra 14d agoI think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.