3 ms·
It helps in two ways: 1) You have to specify your system, right? With TLA+, you can just wave you hands and say "okay this part does something, I guess." You h
by hwayne 9y ago
It helps in two ways:
1) You have to specify your system, right? With TLA+, you can just wave you hands and say "okay this part does something, I guess." You have to force yourself to understand what, exactly, you want your system to do and what you want out of it.
2) Most systems have edge cases, side effects, and race conditions. Are you sure your design is robust against them? You might think you have good arguments for that, but wouldn't it be better to rigorously _check_?
Tests and types and stuff help you find bugs in your implementation. TLA+ helps you find bugs in your blueprints.
- tasuki 9y agoGood points! Writing unit tests before code can help avoid mistakes in the interface design. Perhaps similarly, writing formal specification could expose the holes in your domain understanding.