I read a post by @norootcause about prophecy variables. It does a very good job of demonstrating the need for them. I also think it's funny that, like mathematicians, computer scientists enjoy coming up with unrealistic pathological examples to disprove widely-believed principles (in this case using a queue with countably infinite length). Like a lot of my blog posts it builds up to a big crescendo before realizing that actually explaining the really hard part would double the length of the post, so the readers should just look at the explanation elsewhere. Still a good post and I came away from it with a blurry idea of how I would do the hard part anyway! https://surfingcomplexity.blog/2024/09/22/linearizability-refinement-prophecy/

#tlaplus

I'm also reading an older post by @pressron called TLA+ in Practice and Theory (https://pron.github.io/posts/tlaplus_part1). It does have one quote that I think is kind of funny:

>Lamport observes that programming languages are complex, whereas ordinary, classical math is simple. Programming languages need to be mechanically translatable to efficient machine code that interacts with hardware and operating systems, and they are used to build programs millions of lines of code long that then need to be maintained by large and ever-changing teams of engineers over many years. Such requirements place constraints on the design of programming languages that make them necessarily complex, but this complexity is not necessary for reasoning about specifications;...

The bulk of my TLA+ tooling-related work for the past few years has been related to how to parse it, and MAN is it a complicated language to parse! So at least at that level I think most programming languages are simpler than TLA+. They are often designed with an eye toward parse simplicity.

#tlaplus