Recent content on Andrew Helwer
I’ve been a fan of security tokens for a decade now and have accrued quite a collection.
This redundancy isn’t a bad thing, as security tokens are easily misplaced and the only way to recover from a lost token is using a second token that is also registered with the service you’re trying to access.
I use security tokens whenever I can!
SSH authentication, universal…
Despite the title this is less a directive and more a description of what has already happened, and how I came to realize it.
Still, there are many who remember StackOverflow as a revelation in the mid-2010s and think some vestige of those times remain.
They think if they make an effort to distill their confusion into a question and post it there they will be rewarded.
Perhaps some…
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 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…
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…
TLA⁺ was developed by Leslie Lamport, originator of \(\LaTeX\), so it’s unsurprising that TLA⁺ syntax looks pretty \(\LaTeX\)-y.
It’s a very mathy language, with much use of symbols like (among others) \A , \E , /\ , \/ , and \in denoting \(\forall\), \(\exists\), \(\land\), \(\lor\), and \(\in\) respectively.
The language tools include a tla2tex command to format TLA⁺ specs…
TLA⁺ sees a lot of use modeling distributed systems.
The ability to explore all possible interleavings of events makes concurrency simple to reason about.
For this TLA⁺ uses something called finite model-checking, which is really just a breadth-first search through the entire state space.
The key here - and this really must be emphasized - is that the model is finite .
There…
Here I’ll write an ode to two closely-linked FOSS projects that have, recently, absolutely floored me with their competence & quality: Sunshine and Moonlight .
These are used to stream video games over a (usually local) network.
Sunshine is a game streaming server: it runs on your PC as it chugs away doing all the heavy lifting of running the game itself, while Moonlight is a game…
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…
Here’s a short report of a time I used TLA⁺ at work, with interesting results.
TLA⁺ is a formal specification language that is particularly effective when applied to concurrent & distributed systems.
TLA⁺ made it tractable for an ordinary software engineer to reason about a tricky distributed systems problem, and it found a bug introduced by an “optimization” I tried to…
Last weekend I had a conversation with an undergraduate student new to computer science, who was reading CLRS .
“I wish” they said, “that all the pseudocode in my algorithms textbook was just written in Python.”
“Ah” I said, “but textbook authors sometimes want their work to endure beyond a decade.”
“But Python’s been around…
An unusual topic for this blog, but worth boosting to a larger audience: Google Groups is dying.
Its epitaph is not yet inscribed on the Killed by Google website, but the end is easily seen from here (although it should also be noted its death was called as early as 13 years ago ).
The deficiencies in Google Groups search, supposedly Google’s forte, have long been noted.
Lately…
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…
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…
2021 saw the completion of my first substantial free software project: a TLA⁺ grammar for tree-sitter , the error-tolerant incremental parser generator.
The project stabilized & found users over the course of 2022, then over the holidays I used it to build the TLA⁺ Unicode Converter .
The new year is a time to reflect on the past and look to the future, so here in early 2023 seems ideal to…
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…
It’s hard to find a textbook series garnering more effusive praise than The Little Schemer , The Little Prover , The Little Typer & co.
 The Little Typer introduces dependent type theory and is the first of the series I’ve read.
I quickly grew to appreciate & enjoy its dialogue-based presentation - I’m a real convert!
I might release future didactic blog posts as a…
Republished from Teleport’s official blog ( link ). I received compensation from Teleport for writing this post. 
 Z3 is a satisfiability modulo theories (SMT) solver developed by Microsoft Research.
With a description like that you’d expect it to be restricted to esoteric corners of the computerized mathematics world, but it’s made impressive inroads addressing…
Interpretations of quantum mechanics are boring. Boring!
Maybe the universe has a strict partition between quantum and non-quantum.
Maybe there are a bunch of parallel universes with limited crosstalk.
Or maybe it’s whatever the Bohmian mechanics people are talking about.
Shut up and calculate, I think.
I don’t say this out of some disdain for idle philosophizing or…
In which I am stunted upon by coin flips 
 Wasn’t too long ago that I felt pretty good about my knowledge of distributed systems.
All someone really needed in order to understand them, I thought, was a thorough understanding of the paxos protocol and a willingness to reshape your brain in the image of TLA⁺.
Maybe add a dash of conflict-free replicated datatypes, just so you know…
This isn’t going to be a post about how adopting a several-thousand-year-old practice can make you a better servant of capital .
Instead, let’s talk about when I feel the lowest of the low.
It comes after spending any number of hours on my computer, maybe even a full day, endlessly circling around different websites in search of stimulation, the quick jolt that comes with…
The headlines don’t lie.
 Microsoft , Google , Amazon , Facebook , and a whole host of other tech companies have announced employees will be working from home until early-mid 2021.
There are reasons to believe this will be pushed back; even if the staggeringly ambitious timelines for vaccine development are met, a vaccine might not be a silver bullet and the pandemic could require…
Note: this post was written for Lean 3; the latest version, Lean 4, is a very different language. 
 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…
Quantum Computers: Not Just for Breaking RSA 
 There’s no denying it, Shor’s algorithm was a blockbuster result.
The thought of an exotic new computer breaking all widely-used public-key crypto plays well with the public imagination, and so you’d be forgiven for believing quantum computing is ultimately a sort of billions-dollar make-work project for software engineers:…
Measurement and signaling in the nonlocal world 
 Popular understanding of quantum mechanics usually focuses on three learning objectives: 
 
 At small scales, particle properties (position, momentum, spin, etc.) are in superposition - they don’t have a definite value, but instead are “smeared” across multiple possible values. 
 Measuring a superposed particle…
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…
Why are we here? 
 What guarantees does formal verification provide?
This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all! 
 What do we mean by software correctness? 
 There are precisely two different ways for a piece of software to be correct: 
 
 The supreme deity of the universe descends from the heavens…
Résumé: Andrew Helwer 
 Self-directed software engineer with over a decade of professional experience.
Particularly passionate & effective when working with distributed systems and formal methods - especially TLA⁺ or Z3.
My development style heavily emphasizes testing, both through the manual creation of large test corpora and automated property-based tests.
Recently deepened…