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.