Skip to Content

Projects

Teaching Projects

I primarily focus on formal methods, the discipline of proving software and systems correct. I work to make these tools more accessible and usable to mainstream industrial computing. While I focus on two tools, TLA+ and Alloy, I’ve also done considerable work for other languages.

TLA+

I also wrote the Learn TLA+ website, arguably the best introduction to TLA+ and industrial formal methods available. Before that I wrote Practical TLA+, which was published under Apress.

Alloy

As part of my commitments to the Alloy board, I maintain a set of free online documentation. Before Alloydocs, the only way reference for Alloy was the Software Abstractions. Now comprehensive documentation is freely accessible to anybody.

Let’s Prove Leftpad

Let’s Prove Leftpad is a collection of implementations of leftpad, formally verified as correct with 18 different theorem provers. Each proof comes with an explanation of how the tooling works, how to understand the proof, and how to set up everything for yourself. It’s one of the best introductions to the practice of formal verification, as well as a great way to compare and contrast the various tools.

We’re always looking for new submissions.

Research Projects

While my blog contains many research projects, these were the most involved: months of research, direct interviews, etc.

The Crossover Project

2019–2021

Is software engineering really a branch of engineering, and what makes us different from other engineers? Dissatisfied with the present online discourse on this question, I interviewed 17 people who worked professionally as both a software engineer and a “real” engineer. I published what I learned in three essays:

  • Are We Really Engineers?: An introduction to the project, what it means to be an engineer, and whether we count.
  • We Are Not Special: Comparing and contrasting the constraints of our work from that of other engineers, and how we’re not all that different in the end.
  • What engineering can teach (and learn from) us: Some of the principles of engineering we have yet to fully adopt and some of the innovations we made that can revolutionize other fields.

A Brief Introduction to Esoteric Languages

2021

A general introduction to “esolangs”, programming languages created for artistic, recreational, or explorative purposes. Covers over a dozen such languages, with deeper dives into the runtime model of five. Consists of a 20-minute video and a 4,000 word companion. The two complement each other but each is also a complete resource by itself.

This is How Science Happens

2019–2020

Is there empirical evidence that some programming languages lead to fewer bugs than others? The story of one high-profile study, the controversy around it, and how it was eventually torn apart. Emphasis on the process and social norms of scientific research.

STAMPing on event-stream

2018–2019

In 2018 the NPM event-stream package was compromised and used in a supply-chain attack. Most people either blamed it on the ex-maintainer of the package or the end-users who included it in their code without auditing. I decided to do a full accident analysis, modeled after Nancy Leveson’s STAMP model. The final analysis is over 8,000 words and identifies 15 different system factors that made the attack possible.

Miscellaneous

Computer Things

My newsletter. Currently updates at least once a week, sometimes twice.

Freelance Work