Writing¶
Recent posts from the blog:
- What 320 Lanes Taught Us About 4 — when you can't fit what you want, remove the thing that seems like it's helping
- The Proof That Caught a Wire — when native_decide returns false, the bug is real
- Intervals Collapse to Points — what happens to formal verification when the hardware is deterministic
- The Snow That Wasn't Bandwidth — when the obvious diagnosis is wrong, the real bug is always simpler
- 120x in an Afternoon — three multiplicative improvements that each looked trivial on their own
- Neither Theory Alone — an SMT solver with one theory is a SAT solver with opinions. Add a second theory and you need a protocol for disagreement
- One Oracle, Four Products — a SAT solver answers one question: is this set of clauses satisfiable? Four crates — the solver itself, a bounded model checker, an SMT solver, and a property-directed reachability engine — are built on that question, each posing it differently
- The Spec That Ate Its Registers — how a 62-register diagnostic braindump fed itself to an architecture and came out as 9 peripherals
- Debugging by Flashlight — when your diagnostic output shares a data path with the thing that's broken, you're debugging in the dark
- Zero New Opcodes — the entire warp scheduler fits in CSR space — no new decode logic, no new pipeline paths, no new encoding pressure
- From Falsification to Minus Thirty-Seven Percent — the best research instrumentation gets built to test hypotheses that turn out wrong
- Every Constraint Was a Door — the hardware limits that killed the original roadmap turned out to unlock a better one
- Twenty Soft Constraints — when a formal model collapses composition and improvisation into one parameter
- The Constraint You Already Had — when the correctness machinery turns out to be the scheduling machinery
- Compose From the Bass — why "know your bottleneck" isn't enough, and what a metal bassist accidentally teaches about GPU programming
- A Fourth Point in the SIMT Divergence Design Space — a divergence model the industry skipped, from type theory to silicon
- Why the Kaleidoscope Looks Symmetric When It Isn't — a fragment shader, a CRT filter, and the scale gap between mathematics and perception
- The Bug That Wasn't There — a one-line soundness hole that zero tests caught and zero users triggered
- What the Type Erases To — a type system that compiles to nothing is not overhead you tolerate — it is proof the compiler can verify and then discard
Software¶
- mm-warp — Native Wayland remote desktop for COSMIC — 4K H.264 streaming
- mm-dream — GPU-accelerated kaleidoscope screensaver — WGSL + libcosmic
Research¶
- warp-core — Soft GPU on ECP5 — 4-warp D4 pinwheel + 9-core J1 Forth mesh
- warp-types — Linear typestate for GPU divergence — compile-time shuffle safety