A Field Guide to Bugs Software bugs predate software. Edison used the word in an 1878 letter, eighty years before the Harvard moth and sixty before the modern computer. What he named has outlasted him

Book Review: What We Can Know Ian McEwan has described What We Can Know as "science fiction without the science," which is both a fair warning and a precise advertisement. The novel is set in 2119. Ri

Book Review: There Is No Antimemetics Division There is a particular flavor of horror that only people who work with information for a living can fully appreciate. It is the horror of data loss, of si

Book Review: Piranesi Susanna Clarke's Piranesi is a book about a man who lives in a House. The House has an infinite number of marble halls. Ocean tides flood the lower floors. Clouds drift through t

Optimal Caverna Gameplay via Formal Methods You know what's better than gloating after winning a board game? Winning every possible board game. And you know what's better than that? Having a machine-c

Can Opus 4.6 do Category Theory in Lean? I have a little category theory library I've been dragging around for about a decade now. It started life in Haskell, got ported to Agda, briefly lived in Idri

A truly omniscient deity would prove itself through computational complexity, not faith—providing mathematically verifiable signatures rather than miracles.

Four readable Rust implementations of type systems from Algorithm W to dependent types, designed as starting points for building type checkers.

LLMs won't replace programmers; they're powerful but flawed tools requiring expert guidance, not autonomous coding savants as hyped by influencers.

AI tools are genuinely useful for developers, but the speculative hype and quasi-religious fervor around them has become unsustainable—a bubble burst would benefit software's future.

Modern life pits our ancient brains against profit-driven algorithms designed to capture attention; the only real solution is to completely opt out.