4 ms·

Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract ov

Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract over the uninteresting parts.

pmiller2 7y ago
That seems like it just pushes all the bugs into the “uninteresting” parts.
- AlexCoventry 7y ago
  Not really. Some parts are harder to reason about than others, especially interactions between components of a distributed system.
- hwayne 7y ago
  It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."