Andrew Helwer

I was reading Hillel Wayne’s new post TLA+ Won’t Solve Everything and became fixated on one of the things he says cannot be expressed in TLA⁺: Possibility and reachability properties: that it’s always possible to make P true, even if you don’t actually de…

Here are my thoughts on the free online textbook Is Parallel Programming Hard, And, If So, What Can You Do About It?

This post stems from a recent conversation with Heidi Howard where we talked about the changing role of TLA⁺ & finite-state model checking in both research and industry.

I’ve been a fan of security tokens for a decade now and have accrued quite a collection.

Despite the title this is less a directive and more a description of what has already happened, and how I came to realize it.

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.

The 2025 TLA⁺ Community Event was held last week on May 4th at McMaster University in Hamilton, Ontario, Canada.

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.

TLA⁺ was developed by Leslie Lamport, originator of \(\LaTeX\), so it’s unsurprising that TLA⁺ syntax looks pretty \(\LaTeX\)-y.

TLA⁺ sees a lot of use modeling distributed systems.

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.

I will here indulge in the traditional practice of using my blog to talk about how I’m using my blog.

Here’s a short report of a time I used TLA⁺ at work, with interesting results.

Last weekend I had a conversation with an undergraduate student new to computer science, who was reading CLRS.

An unusual topic for this blog, but worth boosting to a larger audience: Google Groups is dying.

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.

Here’s a short post about two bugs I wrote while writing C++ code for the external scanner of my TLA⁺ tree-sitter grammar.

2021 saw the completion of my first substantial free software project: a TLA⁺ grammar for tree-sitter, the error-tolerant incremental parser generator.

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.

It’s hard to find a textbook series garnering more effusive praise than The Little Schemer, The Little Prover, The Little Typer & co.

Republished from Teleport’s official blog (link).

Interpretations of quantum mechanics are boring.

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.

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.

The headlines don’t lie.

Note: this post was written for Lean 3; the latest version, Lean 4, is a very different language.

Quantum Computers: Not Just for Breaking RSA There’s no denying it, Shor’s algorithm was a blockbuster result.

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

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.

Why are we here?