Composing TLA+ Specifications with State Machines

All of my budgeted blogwriting time is going to Logic for Programmers. Should be back early 2025. (I’m still writing the weekly newsletter.)

A toolbox language is a programming language that’s good at solving problems without requiring third party packages. My default toolbox languages are Python and shell scripts, which you probably already know about. Here are some of my more obscure ones. AutoHotKey Had to show up! Autohotkey is basically “shell scripting for GUIs”. Just a...

In his book On War, Clausewitz defines friction as the difference between military theory and reality: Thus, then, in strategy everything is very simple, but not on that account very easy. Everything is very simple in war, but the simplest thing is difficult. These difficulties accumulate and produce a friction, which no man can imagine exactly...

I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall. Everything in the main post applies to all formal specifications, everything in dropdowns is for experienced Alloy users. Consider a simple model of a dependency tree. We have a set of top-level dependencies for our program, which have their...

It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different what you usually do. For example, last year I talked about the strangest markets on the internet. This year I went down a different rabbit hole. Daniel has been a top 5 baby name twice since 2000. There are over 1.5 million Daniels...