Latest posts
- A sufficiently comprehensive spec is not (necessarily) codeApr 15, 2026
Sorry for missing last week! Was sick and then busy. This week I want to cover a pet peeve of mine, best seen in this comic: A "comprehensive and precise spec" is not necessarily code. A specification corresponds to a set of possible implementations, and code is a single implementation in that set. As long as the set has more than one element, there is a separation between the spec and the code.
- April Cools Post: New York vs Chicago PizzaApr 01, 2026
Happy April Cools! My not-tech post this year is Chicago vs New York Pizza is the Wrong Argument, which is mostly an excuse for me to talk about Chicago food. See here for all of the other April Cools submissions. As of this email we have sixteen posts; there's still time to submit something!1 This one came out of a pizza argument with Marianne Bellotti, a true New Yorker who doesn't think deep di
- Choose Boring Technology and Innovative PracticesMar 24, 2026
The famous article Choose Boring Technology lists two problems with using innovative technology: There are too many "unknown unknowns" in a new technology, whereas in boring technology the pitfalls are already well-known. Shiny tech has a maintenance burden that persist long after everybody has gotten bored with it. Both of these tie back to the idea that the main cost of technology is maintenan
- LLMs are bad at vibing specificationsMar 10, 2026
No newsletter next week I'll be speaking at InfoQ London. But see below for a book giveaway! LLMs are bad at vibing specifications About a year ago I wrote AI is a gamechanger for TLA+ users, which argued that AI are a "specification force multiplier". That was written from the perspective an TLA+ expert using these tools. A full 4% of Github TLA+ specs now have the word "Claude" somewhere in them
- Free BooksMar 03, 2026
Spinning a lot of plates this week so skipping the newsletter. As an apology, have ten free copies of Logic for Programmers. These five are available now. These five should be available at 10:30 AM CEST tomorrow, so people in Europe have a better chance of nabbing one. Nevermind Leanpub had a bug that made this not work properly
- New Blog Post: Some Silly Z3 Scripts I WroteFeb 23, 2026
Now that I'm not spending all my time on Logic for Programmers, I have time to update my website again! So here's the first blog post in five months: Some Silly Z3 Scripts I Wrote. Normally I'd also put a link to the Patreon notes but I've decided I don't like publishing gated content and am going to wind that whole thing down. So some quick notes about this post: Part of the point is admittedly t
- Stream of Consciousness Driven DevelopmentFeb 18, 2026
This is something I just tried out last week but it seems to have enough potential to be worth showing unpolished. I was pairing with a client on writing a spec. I saw a problem with the spec, a convoluted way of fixing the spec. Instead of trying to verbally explain it, I started by creating a new markdown file: NameOfProblem.md Then I started typing. First the problem summary, then a detailed
- Proving What's PossibleFeb 11, 2026
As a formal methods consultant I have to mathematically express properties of systems. I generally do this with two "temporal operators": A(x) means that x is always true. For example, a database table always satisfies all record-level constraints, and a state machine always makes valid transitions between states. If x is a statement about an individual state (as in the database but not state mac
- Logic for Programmers New Release and Next StepsFeb 04, 2026
It's taken four months, but the next release of Logic for Programmers is now available! v0.13 is over 50,000 words, making it both 20% larger than v0.12 and officially the longest thing I have ever written.1 Full release notes are here, but I'll talk a bit about the biggest changes. For one, every chapter has been rewritten. Every single one. They span from relatively minor changes to complete ch
- Refinement without SpecificationJan 20, 2026
Imagine we have a SQL database with a user table, and users have a non-nullable is_activated boolean column. Having read That Boolean Should Probably Be Something else, you decide to migrate it to a nullable activated_at column. You can change any of the SQL queries that read/update the user table but not any of the code that uses the results of these queries. Can we make this change in a way that
- My Gripes with PrologJan 14, 2026
For the next release of Logic for Programmers, I'm finally adding the sections on Answer Set Programming and Constraint Logic Programming that I TODOd back in version 0.9. And this is making me re-experience some of my pain points with Prolog, which I will gripe about now. If you want to know more about why Prolog is cool instead, go here or here or here or here. No standardized strings ISO "str
- The Liskov Substitution Principle does more than you thinkJan 06, 2026
Happy New Year! I'm done with the newsletter hiatus and am going to try updating weekly again. To ease into things a bit, I'll try to keep posts a little more off the cuff and casual for a while, at least until Logic for Programmers is done. Speaking of which, v0.13 should be out by the end of this month. So for this newsletter I want to talk about the Liskov Substitution Principle (LSP). Last wee
- Some Fun Software FactsDec 10, 2025
Last newsletter of the year! First some news on Logic for Programmers. Thanks to everyone who donated to the feedchicago charity drive! In total we raised $2250 for Chicago food banks. Proof here. If you missed buying Logic for Programmers real cheap in the charity drive, you can still get it for $10 off with the holiday code hannukah-presents. This will last from now until the end of the year. Af
- One more week to the Logic for Programmers Food DriveNov 24, 2025
A couple of weeks ago I started a fundraiser for the Greater Chicago Food Depository: get Logic for Programmers 50% off and all the royalties will go to charity.1 Since then, we've raised a bit over $1600. Y'all are great! The fundraiser is going on until the end of November, so you still have one more week to get the book real cheap. I feel a bit weird about doing two newsletter adverts without
- Get Logic for Programmers 50% off & Support Chicago FoodbanksNov 10, 2025
From now until the end of the month, you can get Logic for Programmers at half price with the coupon feedchicago. All royalties from that coupon will go to the Greater Chicago Food Depository. Thank you!
- I'm taking a breakOct 27, 2025
Hi everyone, I've been getting burnt out on writing a weekly software essay. It's gone from taking me an afternoon to write a post to taking two or three days, and that's made it really difficult to get other writing done. That, plus some short-term work and life priorities, means now feels like a good time for a break. So I'm taking off from Computer Things for the rest of the year. There might
- Modal editing is a weird historical contingency we have through sheer happenstanceOct 21, 2025
A while back my friend Pablo Meier was reviewing some 2024 videogames and wrote this: I feel like some artists, if they didn't exist, would have the resulting void filled in by someone similar (e.g. if Katy Perry didn't exist, someone like her would have). But others don't have successful imitators or comparisons (thinking Jackie Chan, or Weird Al): they are irreplaceable. He was using it to des
- The Phase ChangeOct 16, 2025
Last week I ran my first 10k. It wasn't a race or anything. I left that evening planning to run a 5k, and then three miles later thought "what if I kept going?"1 I've been running for just over two years now. My goal was to run a mile, then three, then three at a pace faster than a power-walk. I wish I could say that I then found joy in running, but really I was just mad at myself for being so bad
- Three ways formally verified code can go wrong in practiceOct 10, 2025
New Logic for Programmers Release! v0.12 is now available! This should be the last major content release. The next few months are going to be technical review, copyediting and polishing, with a hopeful 1.0 release in March. Full release notes here. Three ways formally verified code can go wrong in practice I run this small project called Let's Prove Leftpad, where people submit formally verified
- New Blog Post: " A Very Early History of Algebraic Data Types"Sep 25, 2025
Last week I said that this week's newsletter would be a brief history of algebraic data types. I was wrong. That history is now a 3500 word blog post. Patreon blog notes here. I'm speaking at P99 Conf! My talk, "Designing Low-Latency Systems with TLA+", is happening 10/23 at 11:30 central time. It's an online conf and the talk's only 16 minutes, so come check it out!
- Many Hard Leetcode Problems are Easy Constraint ProblemsSep 10, 2025
In my first interview out of college I was asked the change counter problem: Given a set of coin denominations, find the minimum number of coins required to make change for a given number. IE for USA coinage and 37 cents, the minimum number is four (quarter, dime, 2 pennies). I implemented the simple greedy algorithm and immediately fell into the trap of the question: the greedy algorithm only wor
- The Angels and Demons of NondeterminismSep 04, 2025
Greetings everyone! You might have noticed that it's September and I don't have the next version of Logic for Programmers ready. As penance, here's ten free copies of the book. So a few months ago I wrote a newsletter about how we use nondeterminism in formal methods. The overarching idea: Nondeterminism is when multiple paths are possible from a starting state. A system preserves a property if i
- Logical Duals in Software EngineeringAug 27, 2025
(Last week's newsletter took too long and I'm way behind on Logic for Programmers revisions so short one this time.1) In classical logic, two operators F/G are duals if F(x) = !G(!x). Three examples: x || y is the same as !(!x && !y). <>P ("P is possibly true") is the same as ![]!P ("not P isn't definitely true"). some x in set: P(x) is the same as !(all x in set: !P(x)). (1) is just a version of
- Sapir-Whorf does not apply to Programming LanguagesAug 21, 2025
This one is a hot mess but it's too late in the week to start over. Oh well! Someone recognized me at last week's Chipy and asked for my opinion on Sapir-Whorf hypothesis in programming languages. I thought this was interesting enough to make a newsletter. First what it is, then why it looks like it applies, and then why it doesn't apply after all. The Sapir-Whorf Hypothesis We dissect nature alon
- Software books I wish I could readAug 06, 2025
New Logic for Programmers Release! v0.11 is now available! This is over 20% longer than v0.10, with a new chapter on code proofs, three chapter overhauls, and more! Full release notes here. Software books I wish I could read I'm writing Logic for Programmers because it's a book I wanted to have ten years ago. I had to learn everything in it the hard way, which is why I'm ensuring that everybody
- 2000 words about arrays and tablesJul 30, 2025
I'm way too discombobulated from getting next month's release of Logic for Programmers ready, so I'm pulling a idea from the slush pile. Basically I wanted to come up with a mental model of arrays as a concept that explained APL-style multidimensional arrays and tables but also why there weren't multitables. So, arrays. In all languages they are basically the same: they map a sequence of numbers (
- Programming Language Escape HatchesJul 24, 2025
The excellent-but-defunct blog Programming in the 21st Century defines "puzzle languages" as languages were part of the appeal is in figuring out how to express a program idiomatically, like a puzzle. As examples, he lists Haskell, Erlang, and J. All puzzle languages, the author says, have an "escape" out of the puzzle model that is pragmatic but stigmatized. But many mainstream languages have esc
- Maybe writing speed actually is a bottleneck for programmingJul 17, 2025
I'm a big (neo)vim buff. My config is over 1500 lines and I regularly write new scripts. I recently ported my neovim config to a new laptop. Before then, I was using VSCode to write, and when I switched back I immediately saw a big gain in productivity. People often pooh-pooh vim (and other assistive writing technologies) by saying that writing code isn't the bottleneck in software development. Re
- Logic for Programmers Turns OneJul 08, 2025
I released Logic for Programmers exactly one year ago today. It feels weird to celebrate the anniversary of something that isn't 1.0 yet, but software projects have a proud tradition of celebrating a dozen anniversaries before 1.0. I wanted to share about what's changed in the past year and the work for the next six+ months. The Road to 0.1 I had been noodling on the idea of a logic book since th
- Logical Quantifiers in SoftwareJul 02, 2025
I realize that for all I've talked about Logic for Programmers in this newsletter, I never once explained basic logical quantifiers. They're both simple and incredibly useful, so let's do that this week! Sets and quantifiers A set is a collection of unordered, unique elements. {1, 2, 3, …} is a set, as are "every programming language", "every programming language's Wikipedia page", and "every fun