Last month I announced my new book, Logic for Programmers, is now available in print. It's long overdue to talk about what this book actually is and why I think most software engineers would find it worth reading. There are two fields of math indispensable to programmers. The first, arithmetic, concerns manipulating numbers. Everybody learns this in grade school. The second, logic, concerns manipulating boolean expressions. A few lucky programmers learn this in college math classes, and everybody else picks it up through osmosis. So the book starts with a crash course in logic, maybe 16 pages of basic math. Then, because this is logic for programmers and not for academics, the next 200 pages are all applications. How to refactor better, how to test better, how to make better data models, etc. So, what do you actually get by learning logic? Three things. First, it opens up a lot of useful software techniques. Once you know some logic you can do things like property-based testing, constraint solving, goal planning, requirements analysis, lots of fun stuff. In particular, formal methods is extremely hot in AI right now, and do to basically anything with FM you need to know logic. Your clanker might be able to clank its way through the implementation details but you need to know the fundamentals to make it implement the right thing. That's why three chapters of the book are on various aspects of formal methods. Second, logic unifies different-seeming ideas in different areas of software. Did you know there's a deep connection between the Liskov Substitution Principle, database migrations, and Hyrum's law? Did you know that the "Rule of Least Power" and "Make Illegal States Unrepresentable" are consequences of the same essential tradeoff? Third, knowing logic just helps you understand stuff better. One database expert said the book had the most lucid explanation he's ever seen of inner and outer joins. But that explanation only works because the book already taught set builder notation and Cartesian products, after which it's pretty easy to formally define joins! So, if you want a deeper understanding of your craft and exposure to lots of cool and useful techniques, I'd strongly recommend learning logic. As for why to learn it from my book? Because it incorporates feedback from fourteen domain experts and fifteen public alphas. I spent three years of my life making this the absolute best book on the subject I could write. You can buy Logic for Programmers as a PDF, epub, or stack of bound paper. Check out the link for more info and a free sample! logicforprogrammers.com/

I feel the same way when I meet a developer that doesn't know about temporal existential hiding in specification refinements. It's like software development 101

New model announcements should preregister their benchmarks like medical trials do "Timefarble 9.6-smash got 82.9 on SplumpkinBench and Opus 5.5 got 80.3!" I know what all those words are supposed to mean and have learned NOTHING

What’s most interesting to me is we have hit half a dozen bugs **not** found by LLMs statically reasoning over code. There is alpha yet

Shabbat shalom

I don't understand people who say that AI makes vim/neovim useless. Neovim is the single best text editing tool I've ever used, and prompts and plans are just screens of text. Are you seriously writing your plan.mds in nano

Your daily reminder that Dunning Kruger isn't actually a real thing

Allow me to share with you the most cursed problem in all of computer science. Take an initial vector, like <1, 2>. Take a goal vector, like <3, 1>. Take a set of addition vectors, like {<1, -1>, <-1, 2>}. Can you, starting from the initial vector and applying addition vectors one at a time, reach the goal vector? This problem is NP-complete, meaning there's no known algorithm to that solves it "efficiently". Now, let's make one tiny change the problem: at no point can any of the elements of a vector go below zero. So if you had <3, 4, 1>, you couldn't add <2, -6, 8>, because that would make the middle element go below zero. This is called a "Vector Addition System", and the problem is the "VAS reachability problem". The good news is the problem is still decidable. For any reachability problem, there's an algorithm you can follow that will eventually tell you if it's reachable or not. Eventually. Because VAS reachability isn't NP-complete anymore. It's Ackermann-complete. How hard is that? Here are the first N terms of the Ackermann function: A(1) = 1+1 = 2 A(2) = 2*2 = 4 A(3) = 3^3 = 27 A(4) = 4^^4 = 4^4^4^4 = 4^(2^512) A(5) = 5^^^5 = 5^^5^^5^^5^^5 etc Most computationally-hard problems are really difficult to explain to people. VAS reachability is unimaginably harder than anything I've ever seen before, and yet can be explained to a fifth grader. That's why it's so cursed.

Like this tweet if you would listen to the @lexi_lambda / @sliminality podcast where we just shoot the shit about PL, software, and other technical esoterica as strikes our fancy Reply if you would volunteer to edit an episode >:)

So what's the over/under on Microsoft and Meta releasing true frontier models in the next year or so Google caught up so it's not "literally impossible"

Say you have a program that, I don't know, automatically computes and outputs blood rituals to summon dread gods. It works correctly but keeps finding rituals that take three gallons of goat blood, and your cooler only has room for one. Rather than buy a bigger cooler, you decide to add a `--max-blood` flag. Putting a constraint on max blood trades compute time (it takes longer to find a ritual) for cheaper outputs (less goat blood). Now, here's a question: how do you know that the cheaper recipes is equally-effective? Maybe the output from `python ritual..py yarlsnarth` binds The Beast That Eats The Sun indefinitely, while adding `--max-blood=1gal` gives a ritual only binds it for sixteen seconds. Hope you didn't need the sun! In other words, we want ritual ingredients to be dependent on the `--max-blood` flag, but the binding time to be independent. Dependence and independence properties come up a lot in formal methods and systems in general. In this particular case, the independence between "binding time" and "max blood" is a metamorphic relation, or a property on the relationship between two function calls. We can formalize the independence (disregarding "no ritual found") as `forall d in dread gods, n in nat: ritual(d).binding_time == ritual(d, max-blood: n)` What's cool here is that you don't need to know in advance what any particular dread god's ideal binding time is, so you can generalize your test over hundreds of different gods. What's less cool is that for any particular dread god, knowing that `--max-blood` doesn't change the binding time is less useful that knowing what that binding time actually is. Metamorphic testing cover more inputs, but are less specific about what they assert. This is a near-universal tradeoff in all testing strategies. (Another common metamorphic relation is "restriction". Say our program kept finding new rituals for the same dread god. Then anything `--max-blood` finds should also be findable without that flag. This maps to a real bug found in Spotify search!) The stateful system equivalent of a metamorphic relation is the hyperproperty. Which I what I originally wanted to talk about (along with how we can explore them in @AntithesisHQ), but then my example went a bit sideways. See also differential testing, where you make sure your vibeporting of MUMPS to rust doesn't break anything by writing tests that all inputs give the same output

People say AI is gonna kill SaaS but what I really think is gonna happen is we're gonna get more SaaS with strong APIs and plugin frameworks. You still get customization, slopcannon writes 1% as much code, someone else still manages maintenance and infra for you

1. A student from Waterloo emailed me asking for advice 2. Replied 3. Got an AI-generated reply, very clearly templated 4. Looked back: the original email was probably AI-written 5. This is how you wreck cold email for everyone else, even from univesity domains Dead internet

What if saying `claude build me a cloud platform make no mistakes` actually worked??? With the newest Antithesis release we have closed the loop and enabled agents to ship reliable systems: antithesis.com/blog/2026/tim…

Okay yesterday's "here's a failed proof of the halting problem" tweet is getting a lot of juice and a lot of questions about the halting problem, so I might as well link two articles I wrote on it. 1) "What does 'Undecidable' mean, anyway": an explanation of the CS concept of "undecidability", Rice's theorem, and the practical consequences of the halting problem being undecidable. buttondown.com/hillelwayne/a… 2) "Turing kicked us out of heaven": what computing would be like if the halting problem was decidable, what cool things we'd be able to do, and why "just give it a timeout" is not a valid bypass of the halting problem. buttondown.com/hillelwayne/a… Give them a read! Halting and undecidability are super cool and underexplained topics.

People keep asking me how many times I open neovim a month these days now that AI is around. It's zero I've been stuck in NeoVim for literally 10 years. Someone please send help. I cannot get out. I'm desperately trying to get out and I can't figure it out. Even the AI is confused. We're both stuck in command mode, in terminal mode, and we can't leave. Nobody knows what the shortcut is. Help please. Help, help, help.