ahelwer

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.

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.

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+.

Unfortunately a lot of us will die in comparable ways if we are lucky enough to get that old. My grandmother was healthy & mentally with it until stroking out in her garden one day at the age of 90. That is the best any of us can hope for and the reality will almost certainly be far more painful and prolonged.

The last I learned of this was at the talk Temporal specification languages in industrial hardware verification by Simon Jantsch of Siemens at the ETAPS 2025 industry day track. Unfortunately I can't find the video posted anywhere, but predominantly the talk spoke of using proprietary symbolic model checkers for Linear Temporal Logic (LTL). It is reasonable to call TLA+ a successor to LTL, although LTL is definitely still used.

The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).

That battle has unfortunately been lost and different sources give different definitions, often exactly swapped. This was discussed in one of the HN posts linked in the article: https://news.ycombinator.com/item?id=36318280

In the end I don't think it is too much of an issue. What confusion is really brought by conflating parallelism and concurrency? Sure, concurrent programs can be serialized onto a single core (that's how deterministic simulation testing implementations like Antithesis and record & replay implementations like Mozilla's rr operate). But there isn't some deep conceptual unlock you get by having a strict conceptual boundary between concurrency and parallelism.

You need root in order to overwrite sudo in the first place I think, but yes password replay attacks are real. This is why I think it is a good idea to get a yubikey and use PAM to require a physical user presence check to acquire root privileges. You don't even need a password at that point. Unfortunately haven't figured out how to make this work over SSH.

An alternative reading of these comments is "I went to the casino and had a great time! Don't understand how you could have lost money."

There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-clock time. So really this just increases the size of the state space people will explore, which might be the difference between checking, say, 3 vs. 5 nodes in a distributed system.

That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next states. I wonder how well this highly unusual side-effectful pattern can be captured in Truffle.

Edit: okay the more I look into GraalVM the more impressed I am. I will have to sit down and really go through their docs. Oracle was actually cooking here.

Hillel Wayne wrote https://learntla.com/ which is quite good! Leslie Lamport also has a webpage of other possible learning resources, including a video course he put together where he wears many strange hats: https://lamport.azurewebsites.net/tla/learning.html

Personally I learned by reading the first few chapters of Specifying Systems.

There are some proposals floating around to evolve PlusCal. Probably the most prominent is Distributed PlusCal[0]. There's a programming language lab at UBC which is also doing a lot of experimentation with transpiling PlusCal to Golang[1]. They presented a paper at the latest community event.

The PlusCal-to-TLA+ transpiler is considered part of the core TLA+ tools and will definitely keep being maintained.

[0] https://conf.tlapl.us/2020/03-Heba_AlKayed-An_Extension_of_P...

[1] https://distcompiler.github.io/

There has definitely been a focus on improving developer onboarding in the past few years! If someone's PR is rejected now that can be considered a failure of the process, something to be fixed. I think when TLA+ was mostly a product of MSR this sort of thing could kind of fly (still unfortunate) but now that we're out in the wild with a foundation it's really a survival thing to not bounce willing contributors.

Hillel Wayne wrote a post[0] about this issue recently, but on a practical level I think I want to address it by writing a "how-to" on trace validation & model-based testing. There are a lot of projects out there that have tried this, where you either get your formal model to generate events that push your system around the state space or you collect traces from your system and validate that they're a correct behavior of your specification. Unfortunately, there isn't a good guide out there on how to do this; everybody kind of rolls their own, presents the conference talk, rinse repeat.

But yeah, that's basically the answer to the conformance problem for these sort of lightweight formal methods. Trace validation or model-based testing.

[0] https://buttondown.com/hillelwayne/archive/requirements-chan...)

I think it is good that people put in a lot of effort to collect this in one place. The report opens with a very strong perspective:

>The case against Stallman is clear, and yet the free software community has failed to act, in particular at the level of institutions and leadership but also in the form of grassroots support for Stallman. Many defenses of Stallman rely on a comfortable ignorance: ignorance of the scope and depth of Stallman’s political campaign against women and victims of sexual violence, or a comfortable belief that Stallman ceased his problematic behavior following his 2021 re-instatement in the Free Software Foundation. Some believe that Stallman’s speech has not caused material harm, or that his fringe views are not taken seriously; we provide evidence to dismiss all of these arguments in this report.

One thing I have consistently encountered when discussing contentious topics with people is that intentional ignorance is a tactic. One cannot be held responsible for acting one way or another on an issue if they do not know anything about it. Women I know in industry report this as by far the most common reaction of male coworkers to one of their colleagues facing allegations of sexual harassment. They don't know anything about it, it seems complicated, they haven't followed it closely, they don't want to get involved, etc. It is very frustrating and I am glad the report has identified this phenomenon and is pointing out this has been going on for long enough that it cannot be reasonably deployed by anybody.

This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!

I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed me saying they found it and it helped them. https://ahelwer.ca/post/2022-10-13-little-typer-ch9/

Good way to describe it. I tend to see it occur on lists alongside The Art of War and The Prince, which have this weird reputation as titanic, dense tomes read by Serious Men but in reality are more like pamphlets that you can go through in about half an hour. The first time I saw a copy of The Art of War in person I actually laughed out loud.

This is a great passage but in a society taking climate change seriously carbon farming will unironically become a thing. Planting certain crops or using certain forms of composting to sequester as much carbon as possible on large areas of land that are not used to produce food or other cash crops.

All modeling suggests that applying both of these tools together (incentives & disincentives) is multiplicatively more effective than applying either on its own. Taxing emissions means those emissions still happened.

Go ahead and buy the land & oil rights to a large oil reservoir if you want to cash in on this hypothetical program.

Paying off the oil companies in this way means the end of the oil companies. They get a one-time cash infusion but that's it, no recurring revenue. Then no more oil companies to lobby against climate change. It's the only non-revolutionary route left, probably. Oil companies aren't just going to stop pumping oil and stop throwing the government around.

It's an actual published paper you can read, not something KSR made up.

If you're still committed to technocratic market-driven solutions to climate change there's the interesting idea of Carbon Quantitative Easing, essentially directly paying people to not emit carbon (read: pay oil companies to not pump out the oil they're going to pump out) or to sequester carbon with various methods. It's thought of as a carrot along with the stick of carbon taxes adding a cost to emissions.

First learned about this in the excellent sci-fi novel The Ministry for the Future.

https://en.wikipedia.org/wiki/Carbon_quantitative_easing

It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.

That's an interesting idea about a built-in ordered opaque value type. You should bring it up at the next monthly TLA+ foundation community call on November 14th![0] It would be interesting to hear peoples' feedback on it.

[0] Details hidden in the google calendar link on this thread in the mailing list: https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfS...

The shortest possible answer is that qubit states are modeled as two-dimensional vectors on the complex unit sphere. We arbitrarily designate two orthonormal vectors on this sphere as corresponding to classical states 0 and 1. If the qubit vector isn't in the 0 or 1 state, it's in some linear combination of them. This is called superposition. Since most people don't know what linear combination means, superposition is explained as "sort of both at the same time". Upon measurement the qubits are collapsed to 0 or 1 with some probability proportional to how close they are to the 0 and 1 states. The precise probabilities are given by something called the Born rule. I gave a longer talk aimed at computer scientists if you're interested beyond this explanation: https://youtu.be/F_Riqjdh2oM

You're talking about the difference between a scientist making like $50-150k/year salary and entities making millions or billions of dollars a year in profit. These are in no way comparable.

I hope this counts as productive feedback if the author of the blog is reading this - the post you put so much effort into writing truly deserves a better presentation experience than this: https://cdn.fosstodon.org/media_attachments/files/110/923/56...

Using a static site generator is surprisingly simple!

Undergraduate physics hasn't changed much in the past two years.