3 ms·

TLA+ is for writing specifications of models, and programming languages are for implementing the models. Sometimes there is very little difference, and sometime

by xtagon 4y ago

TLA+ is for writing specifications of models, and programming languages are for implementing the models. Sometimes there is very little difference, and sometimes there is more. It's subtle in simpler examples like yours but becomes a little more obvious if you watch Leslie Lamport's video course: https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html The magic comes into play when you do things like using solvers (built into the TLA+ toolkit) to check invariants. This wouldn't be possible do with a code implementation alone, except for if you were to write property tests using a property testing framework or scenario generator using knowledge of all states the domain could be in. Your TLA+ specification is a mathematical formula of the states it can be in (even over time) while the Python implementation is more like a state machine that takes one input and results in an output. Of course, in your example, you do something akin to property testing with pytest where you enumerate known states, I'm just using this to help describe the spec/implementation difference. In more complex models, testing property invariants may require enumerating more examples than you think to write tests for, and the important cases may not be what you expect. And as your property testing parameters get more complex in the search space, what your Python code ends up being is both an implementation (the runtime code) and a de-coupled model of the states it can be in (the test code) when conceptually it is one model. And in TLA+, you can specify it as a model and use the invariant checker as both a way to test your assumptions and a way to explore important states or state transitions.

fijiaarone 4y ago
If it takes a programmer in a specific (unused) programming language to write a specification, why not just write it in a working programming language? As we can see from the comment above, we need to write a compiler and tests to check the specification anyway.
- Jtsummers 4y ago
  Python (and most languages) and testing likely won't detect the concurrency bug in the above program, unless you get lucky. TLA+ and model checking will. You use TLA+ to examine a spec or design without the extraneous details and do V&V on it. Then you go back to your code and you can be more confident that what you are making will work as intended. It is complementary, not a full alternative. You'll still want tests for your code.
- hedora 4y ago
  TLA+ lets you express algorthims that solve NP complete problems concisely. In particular, you can naturally say stuff like "this emits an arbitrary member of the set that satisfies this set of equations". Of course, you can't execute such programs efficiently. The hope is that a model checker can efficiently prove they cannot hit an assert failure (halt) or find a counterexample. This is impossible in theory, but often tractable in practice.
- xtagon 4y ago
  You write a compiler and tests to check the Python implementation. If you were to write it in TLA+ you could use a built in solver and specify invariants to check, which are just formulas, without requiring all the boilerplate that a programming language would require in order to be able to simulate examples from the state space. I wouldn't say it "takes" programmers doing it this way. It's just something that can be in your toolbox if it's useful to you. Sometimes there are benefits to being able to iterate quickly on simpler models before diving into code implementations. Sometimes it wouldn't be warranted. Sometimes you can find a multi-step difficult-to-replicate bug in a specification that is modeling what would actually be multiple complex components in a system that might be in totally different programming languages, and testing them all to completion wouldn't be feasible, but testing a model of them might.
- erichocean 4y ago
  > If it takes a programmer in a specific (unused) programming language to write a specification TLA+ isn't a programming language, it's a specification language. Programming languages are much too concrete to evaluate designs; that's why specification languages (like TLA+) exist. You "test" a TLA+ design by running a model checker (usually TLC) that verifies the design meets the spec (i.e. a bunch of invariants which are the TLA+-equivalent of unit tests).

by xtagon 4y ago

fijiaarone 4y ago

If it takes a programmer in a specific (unused) programming language to write a specification, why not just write it in a working programming language? As we can see from the comment above, we need to write a compiler and tests to check the specification anyway.

Jtsummers 4y ago
Python (and most languages) and testing likely won't detect the concurrency bug in the above program, unless you get lucky. TLA+ and model checking will. You use TLA+ to examine a spec or design without the extraneous details and do V&V on it. Then you go back to your code and you can be more confident that what you are making will work as intended. It is complementary, not a full alternative. You'll still want tests for your code.
hedora 4y ago
TLA+ lets you express algorthims that solve NP complete problems concisely. In particular, you can naturally say stuff like "this emits an arbitrary member of the set that satisfies this set of equations". Of course, you can't execute such programs efficiently. The hope is that a model checker can efficiently prove they cannot hit an assert failure (halt) or find a counterexample. This is impossible in theory, but often tractable in practice.
xtagon 4y ago
You write a compiler and tests to check the Python implementation. If you were to write it in TLA+ you could use a built in solver and specify invariants to check, which are just formulas, without requiring all the boilerplate that a programming language would require in order to be able to simulate examples from the state space. I wouldn't say it "takes" programmers doing it this way. It's just something that can be in your toolbox if it's useful to you. Sometimes there are benefits to being able to iterate quickly on simpler models before diving into code implementations. Sometimes it wouldn't be warranted. Sometimes you can find a multi-step difficult-to-replicate bug in a specification that is modeling what would actually be multiple complex components in a system that might be in totally different programming languages, and testing them all to completion wouldn't be feasible, but testing a model of them might.
erichocean 4y ago
> If it takes a programmer in a specific (unused) programming language to write a specification TLA+ isn't a programming language, it's a specification language. Programming languages are much too concrete to evaluate designs; that's why specification languages (like TLA+) exist. You "test" a TLA+ design by running a model checker (usually TLC) that verifies the design meets the spec (i.e. a bunch of invariants which are the TLA+-equivalent of unit tests).