January 11, 2021

How I got into formal methods

Alloy Workshop

There's a couple slots left for the February Alloy Workshop. Feb 8th, 10 AM - 6 PM CST. Learn how to find bugs in your designs without having to spend weeks coding them up first! If you're new here and haven't heard of Alloy before, here's a good demo I made about modeling with Alloy.

How I got into formal methods

A few people have been asking me this recently, so I figured I'd put it in one place:

So first of all, I don't have any formal CS background. I was a double math and physics major in College and took all of two CS courses, one of which was just the mathematics of formal languages. Pretty much everything I know about CS is self-taught. Also, while there's some math in FM, I didn't learn any of it in school, besides maybe how to do proofs and think in math and the like. Almost all the math I learned was on continuous domains, like analysis and differential equations and stuff, things that are really important to physics but mostly useless in programming. I only veered away from physics in my last year, when I realized 1) grad school would break me, and 2) I really liked money.

What I'm trying to say here is that you don't need a strong academic background to use formal methods. Anyway, after bouncing around SF for a bit I ended up back in Chicago, working for an edtech company called eSpark. We made an iPad app that managed education apps for schools. Like a kid would take a common core assessment, we'd find they were weak in adding fractions, so we'd assign them education apps that taught them about adding fractions. The idea is simple. The accidental complexity around it, like dealing with Apple licenses and iPad device management and school budgets and kids trying to eat their iPads, is enormous. There's also a great deal of operational complexity. Usage ramps up during the back-to-school timespan we called "Launch Season", where all of the new schools and classrooms run into all sorts of fun issues getting things working. Launch season is the most stressful time of year.

While the product was an iPad app, it was a wrapper around a website, so the majority of our work was actually in React and Rails. Now, two things about me worth noting:

1. I really love off-the-wall wildly-experimental moonshot projects. "Capacity for skunkworks" was one of the my criteria I used when searching for jobs. At eSpark, I was constantly throwing stuff at walls and seeing what sticks. Maybe a quarter of the time it would be something useful, and the rest of the time it would either fizzle out or prove to be a really bad idea. People were used to me going "what if we migrated everything to Prolog?"
2. I hate doing frontend.

Nothing wrong with frontend, I just don't like it. I'm much happier doing backend stuff. All the other engineers were either fullstack or frontend only; I was the only pure backend. The only team that needed a pure backend person was the team in charge of launch season, so I was put on that.

Then, just before the 2016 launch, one of the other team members quit and another had to be reassigned. I was now the only engineer on the launch season team.

Then, due to a bunch of unrelated factors, launch season 2016 ended up being one one of the toughest I'd ever seen. It was a bad year, and I almost burnt out keeping things running. I also threw a lot of stuff at the wall to see what would stick. Most didn't. It was while investigating... something, maybe Idris (?) that I ran into this argument, which lead to the famous Use of Formal Methods at Amazon Web Services paper, which got me interested in trying TLA+.

Unrelated to all this, I'd been diagnosed with ADD as a teen but only started taking medication that autumn. I'm not sure how many of you have been on Ritalin before, so here's the lowdown: the first couple days on it, you feel like a god. Everything is obvious, everything is easy, you can do just so much. It calms down after that, but those first two days... there's a fire inside you and it superheats your breath.

I spent the first couple hours writing a Vim brainfuck interpreter and the rest of the time teaching myself TLA+. It was really tough going with the material then available, but I kept pushing and eventually got out a couple of specs. Then I decided to try it on some of the launch season problems. There was a lot of pressure in the company to fix things as fast as possible and I wanted to spend more time planning out changes to make sure they didn't cause other problems. Writing a formal spec seemed like a great way to do that!

I think people gave me leeway on this because they knew how stressful the season was on me, and if playing around with an academic project helped me cope a little, worthy tradeoff. So people were quite surprised when it started finding bugs. Because it found a lot of bugs.

I did a writeup of the first major success story here. I still remember the CTO's reaction when I first showed him a bug: "I've been in the industry for ten years and I've never seen anything like this before."

(I think my favorite success story was when we were arguing with a third party vendor over a weird integration bug. They said our integration was breaking shit, we said it was their fault, total impasse. Eventually I got fed up and passed over a spec saying "look, it can't be our problem, we formally proved that our system is correct." Now if they knew anything about formal methods they'd have seen right through this, but they didn't, and it spooked them enough that they actually checked their code for bugs. Surprise, it was their code causing the problems.)

While I now know a lot more about the theory and mathematics in formal methods, I didn't at the time; I just knew that TLA+ was a complicated tool that found complicated bugs.¹ That, more than anything else, is what convinced me that FM could be much more widely used than it was at the time (and still is). So I wrote a tutorial for TLA+, then learntla, then a conference talk, then a book, and now I teach formal methods full-time.

Wanna reiterate here: I started as a webdev. I used formal methods as a webdev. People say FM is for "nukes 'n nasa", and that it's too expensive for more informal domains, but that's wrong. We applied it to a Rails monolith and it saved us a lot of money. It's more that people haven't seriously tried applying FM to informal domains, not that it's inherently unsuitable.

Anyway, that's a quick rundown of how I got into formal methods. Hope you enjoyed! I'll be spending the rest of the week grinding on the Crossover Project. Still a lot to do, but the end is in sight!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.