I love this. This is great to read if you are trying to use TLA+ for something.
In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.
If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.
I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.
I discovered Quint[0] due to this comment[1] on HN. Quint is "an executable specification language [which works in JavaScript] with delightful tooling based on the temporal logic of actions (TLA)". I think it is awesome and anybody interested in TLA+ should check it out.
i think part of this is a shortcoming of our programming languages. generally, languages allow for the expression of partial graphs, which makes the verification problem technically challenging. my take is that a language that only exposes closed-graph semantics could help bridge the gap between the model and the implementation, even if not absolute.
What you say reminds me of the "Von Neumann Languages Lack Useful Mathematical Properties" section in John Backus's Turing award paper. One of his criticisms of what we would now call imperative languages is that they make it exceedingly difficult to formally prove facts about a program.
Great write-up. People keep saying "we can just write tests" or more recently "we can use formal verification," thinking these are sufficient safeguards we can use and then relegate all the implementation to LLMs. But the fact is that probabilistic guessing machines can't save them. People can't escape the need to actually understand the things they are building.
These probabilistic guessing machines are pretty great for creating these formal models, e.g. TLA+, and then guessing if the implementation aligns with the spec.. In fact, it's my go-to tool for constructing soft guardrails for the model, so the design it's going to implement is logically sound. Same as for people: it's easier to make something working when you have a spec that is working.
Of course, it still allows the risk that you don't actually get to understand it.
> People can't escape the need to actually understand the things they are building.
While on the one hand, you do need some kind of grounding in human specification for what to build and what good looks like, any particular defect humans can find should be findable via software.
>> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.
>> Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels
In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.
If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.
[0]: https://github.com/quint-co/quint
[1]: https://news.ycombinator.com/item?id=49865720
https://dl.acm.org/doi/epdf/10.1145/359576.359579
Of course, it still allows the risk that you don't actually get to understand it.
While on the one hand, you do need some kind of grounding in human specification for what to build and what good looks like, any particular defect humans can find should be findable via software.
> From "The Future of TLA+ [pdf]" (2024) https://news.ycombinator.com/item?id=41385141 :
>> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.
>> Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels
The internet discovers TLA+. Now what?
https://news.ycombinator.com/item?id=49863600