Here I’ll talk about a type of TLA⁺ contract I’ve worked on a few times, and why it didn’t work out as well as hoped. I’m not trying to torpedo other peoples’ contracts here - I just hope to share this experience so others can structure their TLA⁺ contracts differently, hopefully leading to greater success for both parties and industry usage of TLA⁺ as a whole. The proposal The contract proposal goes like this: a client wants to build a distributed system, and has read that TL...| Andrew Helwer
The 2025 TLA⁺ Community Event was held last week on May 4th at McMaster University in Hamilton, Ontario, Canada. It was a satellite event to ETAPS 2025, which I also attended, and plan to write about in the near future. I gave a talk somewhat-hucksterishly titled It’s never been easier to write TLA⁺ tooling! which I will spin into a general account of the state of TLA⁺ development here. The conference talks were all recorded, so if you’d like this blog post in video form you can wat...| Andrew Helwer
Although it isn’t usually taught that way, a lot of TLA⁺ newcomers develop the understanding that TLA⁺ is just a fancy domain-specific language (DSL) for breadth-first search. If you want to model all possible executions of a concurrent system - so the thinking goes - all you have to do is define: The set of variables modeling your system The values of those variables in the initial state(s) Possible actions changing those variables to generate successor states Safety invariants you wan...| Andrew Helwer
A few days ago I published a short post about two bugs I wrote while developing the C++ external scanner for my TLA⁺ tree-sitter grammar. Reactions were mixed! Many people were supportive, but there were of course the usual drive-by claims by developers that the bugs were trivial, they would’ve found & fixed them inside of 20 minutes, and I was laughably incompetent for having written them in the first place.| Andrew Helwer
Here’s a short post about two bugs I wrote while writing C++ code for the external scanner of my TLA⁺ tree-sitter grammar. External scanners use handwritten C or C++ code to parse the non-context-free parts of your language. I’ll try not to dump on C++ too hard but both of the bugs are highly ridiculous and exemplify why I hope to write as little of the language as possible for the rest of my career.| Andrew Helwer
Quantum interference in the sum-over-paths formalism| Andrew Helwer
Turn back the clock to 2009: a confused physics major newly infatuated with math and computer science, I enrolled in MATH 273: Numbers and Proofs at the University of Calgary. This wasn’t my first encounter with mathematical proof; in first-year calculus I’d mastered rote regurgitation of delta-epsilon proofs. Despite writing out several dozen, their meaning never progressed beyond a sort of incantation I can summon to this day (for every \( \epsilon > 0 \) there exists a \( \delta > 0 \)...| Andrew Helwer
Quantum chemistry for complete beginners| Andrew Helwer
Lessons I’ve learned from software engineering are uniformly cynical: Abstraction almost always fails; you can’t build something on top of a system without understanding how that system works. Bleeding-edge methods are a recipe for disaster Everything good is hype and you’ll only ever get a small fraction of the utility being promised. Imagine my surprise, then, when the Z3 constraint solver from Microsoft Research effortlessly dispatched the thorniest technical problem I’ve been give...| Andrew Helwer
Written during an interesting time in my life| Andrew Helwer
I will here indulge in the traditional practice of using my blog to talk about how I’m using my blog. This page is built with the Hugo static site generator. I recently updated it to use the latest version of the beautifulhugo theme, which unbeknownst to me included a dark mode colorscheme. Recent browsers use the prefers-color-scheme option to automatically choose light or dark mode CSS styles, if the website supports it.| Andrew Helwer
Author’s note: I wrote this in 2017 and it languished in the drafts since then because I couldn’t think of a good conclusion. Really this is typical of the subject matter and all this piece offers is something to chew on, if you have the interest in it or have never before considered the question. At the time I was helping tutor a TLA⁺ seminar and had the opportunity to ask Leslie Lamport (who has thought about computation quite a bit!| Andrew Helwer
Yes, it's the replace function in chapter 9| Andrew Helwer
