Learn TLA+
hillelwayne.com
hillelwayne.com
The example starts out with a simple piece of code that exposes a bug, then the bug gets fixed and the following question is asked:
> Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything
> The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirements and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct.
[0]: https://www.learntla.com/intro/conceptual-overview.html
> if (from.balance <= amount) # guard
> if acct[from] >= amnt then
This bugfix brings up 2 good points.
1. Using TLA+ is no silver bullet to writing bullet-proof code. Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. I wish there was a translator that'd convert your TLA+ to code in a language of your choice.
2. Say what people may want about centralization (Git vs. Github, etc), this successful micro-collaboration was enabled by this centralization. Someone posts a link to a book/article, someone else posts a deep-link to some example code, yet another person finds bug in the said code, hunts down the Github link, uses Github's in-place edit feature (no (`git clone` + fix + `git push`)) and submits a merge-request, the author merges the fix (and smacks head :-). All this was kicked off by a conversation on HN, a center/hub for conversations.
Having only done the basic tla+ tutorials (not the OP's site yet), this is still my biggest roadblock with even trying to use a formal system. The "impedance mismatch", if you see what I mean. Comparing to automated tests, it seems less likely to get both code and tests wrong in concert, than to get a tla+ spec right, and then botch the translation to code.
I'm sure it's a faq, and the answer probably boils down to "just try it, and you'll see" ?
If your budget allows, it is worthwhile to invest into translation of C or TLA+ code back into specification code. This way you may run specification checks again against backtranslated specification. And you can do that process to a fixed point where nothing changes, neither (back translated) specification code, nor code generated from specification.
I do the online checks because I don't trust the code, so I check (at runtime) that the code matches the specIfor the exact (runtime) situation that code is being run in. If it doesn't, I hang/abort.
No, it's not proving anything. Github Copilot could have definitely made the same mistake.
This isn't a good argument for centralization. Yes, obviously we need to meet in the same "place" for this to happen, but this "place" could just as well be an identifier, for instance a Matrix room. There is no need for the server architecture to be centralized.
Additionally, I don't find your example of in-place editing being much better than `git clone` + fix + `git push` to be very motivating. At best, that's an UX issue, not an inherent benefit of centralization.
The rest of your points actually stand and I agree with them, even when we ignore the misguided call for centralization.
It might seem simple enough, but this bug shows that
if (Current < Withdrawal): Current -= Withdrawal
Whereas
isValidTransaction = Current - Withdrawal >= 0
if (isValidTransaction): NewBalance = Current - Withdrawal
In the first case, the reader is expected to do mental math (albeit easy) in order to verify correctness. Whereas in the second, they're only expected to read a logical statement and confirm that the logic checks out.
Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.
tlc still has some advantages over apalache in some conditions, but actually I've never even used apalache with my models (I'm still in the practice phase, though).
As a TLA non-SME I couldn't say, but would definitely find it useful and probably impressive. Maybe Brad Fitzpatrick could team up with Aphyr and use it to make golang v2 a bit less crap.
Note: I write this with love, as someone who's written hundreds of thousands of lines of Go, and am now turned off and afraid of the behavior at the sketchy edge boundaries. I've now shifted to learning Rust, albeit slowly and finding it saddeningly challenging compared to what I can pump out with the Go.
For reference, see "Data Race Patterns in Go", posted 21 days ago: https://news.ycombinator.com/item?id=31698503
That said, I think the Spin syntax is slightly closer to native Go, making it easier to write specs. At least that's what people who know both Spin and Go tell me. https://github.com/dgryski/modelchecking/blob/master/spin/fi...
One thing that I wish websites did is to make it easy to report simple typos and grammatical errors without having to go through GitHub. For example, on https://www.learntla.com/intro/faq.html "losting" should be "losing". It would be great to simply and quickly report them without having to context switch and go through the overhead of opening an issue or creating a PR. (In any case, I don't even have a GitHub account.)
I wasn't even going to click the link, because I thought this was for the old online book. Because of your comment, I see that Learn TLA+ has been updated, and Hillel says of the Practical TLA+ book I bought a couple of weeks ago: "Don't bother."
I haven't gotten that far yet, but I have modeled the wolf, cabbage, and goat problem, and helped the poor waiter in xkcd 287. Eventually I hope to apply it to a distributed database and our crazy Jira deployment. I'm not sure which will be harder.
I feel like you dropped this.
I'm just finishing cosmic python[0], which talks about making a primitive model of your system first, that you can run business logic tests on, then all the other code depends upon that (domain driven design / onion layers, etc). To me it seems like this is the same thing. The only aspect that stuck out was the "two transfers at the same time" which to me, seems like it would depend on how you're implementing the model, rather than the model itself?
For instance, the example in [1] could also be done in primitive python, (arguably easier to read in my opinion but I'm not used to TLA syntax :)
@dataclass
class Person:
balance: int
def wire(a: Person, b: Person, amount: int):
if a.balance >= amount:
a.balance -= amount
b.balance += amount
@pytest.mark.parametrize(
"a_amount, b_amount, transfer, a_remaining, b_remaining",
[
(10, 10, 10, 0, 20), # matching amount
(6, 10, 10, 6, 10), # has less
(0, 10, 10, 0, 10), # has nothing
(10, 0, 10, 0, 10), # to empty account
],
)
def test_wire(a_amount, b_amount, transfer, a_remaining, b_remaining):
a = Person(balance=a_amount)
b = Person(balance=b_amount)
wire(a, b, transfer)
assert a.balance == a_remaining
assert b.balance == b_remaining
[0]https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html
TLA+ is not a programming language, and so cannot "run," but it is more expressive than any programming language could ever be, and can describe any discrete system at any arbitrary level of detail. This is particularly useful when the described system has some or a lot of nondeterminism, as is the case in distributed and concurrent systems. It is very easy in TLA+ to say "one of these things could happen at any time", or "the value of a variable can only grow monotonically over the system's lifetime", and it is easy to describe assertions of arbitrary complexity about a system, such as "every order that's received more than once will eventually be flagged."
As for tooling, while you cannot efficiently "run" TLA+ specifications, you can check your assertions in two ways: either with the proof assistant (although that requires a lot of effort), or with a model checker, that is places more limitations on what it is that you can check but is completely automatic.
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.
As we can see from the comment above, we need to write a compiler and tests to check the specification anyway.
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.
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.
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.
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).
So take that definition for the wire function and let two processes run it simultaneously:
alice.balance = 100
spawn(wire(alice, bob, 100))
spawn(wire(alice, bob, 100))
p1:
if a.balance >= amount: -- true, so continues into the condition body
a.balance -= amount -- process paused here
b.balance += amount
p2:
if a.balance >= amount: -- true, so continues into the condition body
a.balance -= amount -- alice's balance now 0
b.balance += amount -- bob gets 100
When testing concurrent programs it is a non-trivial thing to force these states, so bugs like this are hard to detect because they may only occur occasionally. And because they occur rarely, even when detected the actual source of the bug can be hard to reliably discern. TLA+'s model checker will check each possible interleaving of the two processes (in this case) and will discover the invalid execution path I showed above. Then you can go back to the spec and address the issue and rerun the checker, if your invariants hold (no sequence of actions lead to overdraft, in this case) then you can have confidence that, at least with regard to the properties you've specified, the system is correct.
Here's what it looks like in Spock:
@Canonical
class Person {
int balance
def wire(Person other, int amount) {
if (balance >= amount) {
balance -= amount
other.balance += amount
}
}
}
class PersonSpec extends Specification {
def 'transferring #amount amount'() {
given: 'two people'
def pa = new Person(balance = a), pb = new Person(balance = b)
when: 'an amount is transferred from a to b'
pa.wire(pb, amount)
then: 'the transfer succeeds if possible, or nothing happens otherwise'
pa.balance == expectedA && pb.balance == expectedB
where:
amount | a | b || expectedA | expectedB
0 | 0 | 0 || 0 | 0
10 | 20 | 0 || 10 | 10
10 | 10 | 10 || 0 | 20
10 | 9 | 10 || 9 | 10
}
}
Also: tests like that can be provably comprehensive in the cases they handle (which can be generated, you don't need to manually list them all), but that was not my point.
Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.
(I don't think it's necessarily the case that they prefer Isabelle or Coq; it really depends on what they're trying to do. I'd be especially fascinated if they prefer, say, SPIN to TLA+, which is a much closer tool.)
A better criticism would probably be to note that TLA+ is even within the more similar world of (say) model checking, it is a LISP to (say) Spin's (or similar) C
What I'll say is a simplification, but I'd describe TLA+ as a one-trick pony, that does that one trick very well. Roughly, you have to structure the model of your algorithm as a transition system, described using a predicate on "these are the legal initial states", and another predicate over two states that says how you can move from one state to the next. To describe these predicates, you get a fairly simple but expressive language at your disposal (a TLA cheat sheet probably fits a single page). This format lends itself well to describing high-level ideas of distributed protocols or concurrent algorithms (roughly what you'd write as pseudocode for those protocols/algorithms). You can then use that same predicate language, plus some additional operators to talk about time (e.g., you can say things like "never" or "eventually"), to specify what your system should do. Finally, you get an automated analysis tool (actually two tools these days, TLC and Apalache), that checks whether your model satisfies the specification. The beauty is that the checking is push-button - after you've finished writing the model and the spec, your work is largely complete. The analysis will have severe limitations; your model can't be too big, and it has to be finite (e.g., if you're writing a model of a distributed protocol, you have to limit the analysis to settings with a handful of nodes), but in practice even this limited analysis weeds out most of the bugs.
Isabelle and Coq are theorem provers (there's also a bunch of other theorem provers). That means, you have to define whatever you're modeling as a mathematical object, and then you go off and prove stuff about it. They're both extremely flexible - you can model a transition system just like TLA does, but you can also talk about any kind of mathematics (algebra, statistics, financial math, whatever). You can also encode programming language semantics, as well as program logics, that allow you both model actual C or OCaml or whatever code, and to specify properties about programs (as mathematical theorems) and prove them in a more comfortable way using program logics. The analysis (which corresponds to proving a theorem) is generally not limited (e.g., you prove a distributed protocol correct for any number of nodes).
The snag is that in Isabelle or Coq the proof is done in a largely manual way (you have to sort of type in the argument by hand, often in excruciating detail). If you want to verify a program with N lines of code, you'll typically end up writing 5-20 times N lines of proof to convince the theorem prover of the correctness of the said program. But to do this, you'll generally have a large library of already proved theorems (6-7 years ago I counted around 200k theorems available for Isabelle), and you will generally have a "metaprogramming language" at your disposal to write your own analysis (i.e., proof) procedures.
For academics, especially programming languages and formal methods people, their work is often writing new programming logics, or new proving procedures, or developing whole new theories. Theorem provers lend themselves better for that kind of work, as well as pushing boundaries, such as doing code-level analysis. But for engineering, TLA can be the 80/20 solution in many cases.
I ctrl+f'd the page and the expansion of that acronym, Temporal Logic of Actions is nowhere to be found.
(Real answer: it's something most of us tell you if you ask, but "Temporal logic of actions" makes it sound a lot more intimidating to learn than it actually is)
We implemented this in medical software for reading patient documents at one of my last jobs, and it's a feature I wish more sites that were focused on reading material had (docs, book replacements, etc.)
Edit: just want to point out this is in no way a critique of this site specifically, so maybe off topic.
Nice to see some new posts on TLA every once in a while. A few days ago someone posted this series of very real-world examples: https://elliotswart.github.io/pragmaticformalmodeling/ It's also quite good.
On a related topic, does anyone know of a comparison to Alloy 6? I've been meaning to take a day or two to look at it (I tried Alloy out a while ago while I was still in my PhD, but have forgotten most of it), I'm curious to see how it stacks up.
Bought the book, FWIW, and love it - but this will help me evangelize TLA+ with my employer and other groups!
The images don't render correctly on macOS safari (v 13.1.3). They are squished horizontally.
I have the Spin book and intend to read it, but I keep having other stuff come up. It's mocking me, I know
Your advocacy for TLA+ makes me want to try it out. I just wanted to understand what I might be getting into.
It could be that you get faster model checking with Spin though, I'm not aware of any comparisons.
If you use Amazon AWS its pretty much guaranteed you'll be using at least one service that's been modelled using TLA+.[1]
[1] https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...