Latest posts
- 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
- You can cheat a test suite with a big enough polynomialJun 24, 2025
Hi nerds, I'm back from Systems Distributed! I'd heartily recommend it, wildest conference I've been to in years. I have a lot of work to catch up on, so this will be a short newsletter. In an earlier version of my talk, I had a gag about unit tests. First I showed the test f([1,2,3]) == 3, then said that this was satisfied by f(l) = 3, f(l) = l[-1], f(l) = len(l), f(l) = (129*l[0]-34*l[1]-617)*l[
- Solving LinkedIn Queens with SMTJun 12, 2025
No newsletter next week I’ll be speaking at Systems Distributed. My talk isn't close to done yet, which is why this newsletter is both late and short. Solving LinkedIn Queens in SMT The article Modern SAT solvers: fast, neat and underused claims that SAT solvers1 are "criminally underused by the industry". A while back on the newsletter I asked "why": how come they're so powerful and yet nobody u
- AI is a gamechanger for TLA+ usersJun 05, 2025
New Logic for Programmers Release v0.10 is now available! This is a minor release, mostly focused on logic-based refactoring, with new material on set types and testing refactors are correct. See the full release notes at the changelog page. Due to conference pressure v0.11 will also likely be a minor release. AI is a gamechanger for TLA+ users TLA+ is a specification language to model and debug
- What does "Undecidable" mean, anywayMay 28, 2025
Systems Distributed I'll be speaking at Systems Distributed next month! The talk is brand new and will aim to showcase some of the formal methods mental models that would be useful in mainstream software development. It has added some extra stress on my schedule, though, so expect the next two monthly releases of Logic for Programmers to be mostly minor changes. What does "Undecidable" mean, anywa
- Finding hard 24 puzzles with planner programmingMay 20, 2025
Planner programming is a programming technique where you solve problems by providing a goal and actions, and letting the planner find actions that reach the goal. In a previous edition of Logic for Programmers, I demonstrated how this worked by solving the 24 puzzle with planning. For reasons discussed here I replaced that example with something more practical (orchestrating deployments), but lef