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.
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 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.
While my blog contains many research projects, these were the most involved: months of research, direct interviews, etc.
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 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.
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.
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.
My newsletter. Currently updates at least once a week, sometimes twice.
- The epistemology of software quality (Increment): Why tools and techniques matter less than you think, and why sleep and safety matter far more.