What TLA+ can and can't check (buttondown.com)

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 think the style guides I’ve seen only permit acquire/release memory orders for locks, and relaxed for simple counters. Anything more complicated including lockless hashtables or RCU, using seq_cst is required by the style guide.

The restriction is a good thing because there are very few humans who can reason about acquire/release semantics in situations other than locks.

Yeah, the last time I had to check anything regarding memory orderings, I wrote a custom analyzer for that problem. It's...not easy. The state space is enormous too, so even with compiled code I had to take some shortcuts and prove parts of the problem by hand.

For C++ GenMC is probably the state of the art for this: https://plv.mpi-sws.org/genmc/

There's also RustMC for Rust.

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.

I wonder if asking an LLM to model their implementation in TLA+ first would improve their implementations.

I recently had this discussion with an energetic junior coworker who just learned about TLA+ and thought it would solve all the problems. I think it probably did give the LLM that he was using to do the actual implementation a better starting off point, but the obvious gap remains, which is whether or not the spec (TLA) matches the implementation (elixir) which there's just not a good answer for. I encouraged him to put his TLA code in our docs folder, because as far as I'm concerned, it's just a suggestion, and then write (and understand...) some property tests about the feature.

I think there probably is some value in vibecoding TLA specs and not actually understanding the invariants yourself, but it's way oversold by the talking heads of the tech world, and the gaps need to be filled in some other way if you refuse to write your own code.

How do managers build software?

The fact is when LLMs get good enough you WILL be able to build software without reading/understanding the code.

Whether or not you think we are already at that point is kind of an unimportant detail.

I would say we are quite close, depending on the type of software you are building.

Speaking as a probabilistic guessing machine who tries to actually understand the thing I'm building, this approach hasn't proven foolproof either.

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.

https://dl.acm.org/doi/epdf/10.1145/359576.359579

> What is the Typst of formal modeling?

I'm not sure there is one, but you can start exploring here:

https://en.wikipedia.org/wiki/Category:Formal_specification_...

For TLA+-styled model checking, though, there is Quint: https://quint.sh/docs/why

It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.

I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.

I feel like PlusCal and TLA+ operate at a different level. I use PlusCal primarily when what I'm modeling has a lot of sequential "A then B then C..." steps. With PlusCal a program counter is implied and it maps more directly to sequential algorithms.

When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".

You should look into Quint: https://github.com/quint-co/quint. It comes with simple syntax and very good developer tooling. Quint to TLA+ is what Typst is to Latex.

You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.

A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.

Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.