Hi, I’m Hillel. I specialize in formal methods for businesses. I’m the author of Practical TLA+, a guide to FM written for industry programmers, and Learn TLA+, a free online resource in the same vein. This blog is a mix of deep dives into formal methods and programming topics I find interesting.
Currently I’m not looking for full employment but am available for consulting opportunities.
You can reach me at h@hillelwayne.com. I always like receiving emails, especially on interesting developments in ESE or new topics to explore. See my open invite.
As of 2020 I’ve written over 130,000 words for this blog. By comparison, The Hobbit is 95,000. Since asking you to read the equivalent of a fantasy doorstop is a little much, here are some of the better pieces I’ve written:
These are the pieces I’m proudest of.
Why do accidents happen? When do we know we’ve dug deep enough? What happens when we look at an accident as a failure of the system instead of chasing the root causes? A 9,000 word primer on accident investigation through the lens of a major npm security attack. We know how to prove code is correct, so why don’t we? People give answers from “websites aren’t airplanes” to “people just don’t care”, but none of these are quite right. An overview of the history of the field, what makes it hard to use in practice, and what we’re doing to change that. On the other hand, maybe there are formal methods that are ready for prime time. In particular, formal specification languages like TLA+ and Alloy can be a huge help for day-to-day programming. Here we take a programming challenge that stumped world-class programmers for weeks… and solve it in just over half an hour.
Okay, you’ve learned how to write your blueprints, but how do you actually apply it? A guide on making specifications useful to you at your job. TLA+ Really nice for concurrent and distributed systems. Things like deploying code, modeling adversarial attacks, and message queues. Alloy Great for domain modeling, formalizing requirements, dealing with highly relational information. Things like procedural content generation, package management, and UI state machines. Decision Tables So lightweight you can teach it to a someone with no programming experience whatsoever. One post on the basics and one on analyzing user requirements.
By studying the history of software, we get a better sense of why things are the way they are.
I got tired of people using the same three people as examples of important woman programmers, so I compiled 20 more. Instead of sharing Ada Lovelace for the 20th time, why not talk about Betty Holberton? She invented breakpoints! In a lot of modern languages, you can write something like x = x + 1. Some people find that weird! I traced the history of where that comes from.
Why everything is terrible.
Scientists don’t write tests, do code review, or even use descriptive names in their code. This makes all science papers that rely on code (ie, most of them) suspect. And then we make policy decisions from them. “Use the right tool for the job” is universally accepted, but what is the right tool anyway? How do we figure it out? Some standards of evidence we can use, ordered by level of rigour (and difficulty).
While formal methods is my specialty, I spend a lot of time reading old papers and digging up obscure technology. Sometimes you find cool stories. Sometimes you find forgotten superpowers. And sometimes you discover a cult.
An incredibly effective means of testing complicated domains like machine learning, computer vision, and expert systems. Has 20 years of development behind it. Why haven’t you heard of it? Academic paywalls. MiniZinc Constraint solving. Give it a bunch of requirements and it spits out a solution. I did a brief intro here. I’m prouder, though, of my essay on getting it to run fast. Probabilistic modeling, letting you say things like “there’s a 20% chance that this will crash.” Powerful verification, sadly limited by very weak expressive power.