Writing¶
Recent posts from the blog:
- A Cap Makes Brute Force Win — we aimed our own IC3/PDR model checker at the split-brain proof expecting it to beat explicit-state enumeration. It lost — because the lease guard caps one quantity, and that collapses the space brute force has to search
- Split-Brain, Unrepresentable — a type can make the bad state impossible to write down and still fail to make it impossible to reach
- Disjoint Becomes Intersecting — generalizing a partition-based type system to a failure-tolerant one is not making the set bigger — it is flipping which set relation the type guards
- Where Structure Ends — a reconfigurable quorum system has two safety mechanisms that look redundant. They are not — they partition the problem by regime
- Up Is Gated, Down Is Free — a value's consensus strength forms a small lattice of levels, and the types that carry it are built from one asymmetry: earning a guarantee demands evidence, discarding one demands nothing
- A Merge Is a Proposal — two committed values disagree and a certified function merges them. The design's central refusal — the result is not a decision — turns out to be a boundary between two literatures: CRDTs (conflict-free replicated data types), where replicas merge freely, and consensus, where they must agree first. Written as a compile error
- The Famous Number Assumes a Signature — every rung of this series assumed nodes fail by stopping. Let them lie, and the evidence has to change type — not size. Along the way, the best-known constant in Byzantine fault tolerance turns out to be licensed by an assumption this toy doesn't get to make
- The Wire Is Where Const Generics Die — every quorum certificate in this crate is indexed by a compile-time epoch; a socket hands you the epoch as eight bytes. What survives that crossing is worth stating exactly
- A Witness Changes Weight — the value lattice commits a value and throws its quorum witness away. Under nodes that lie, that same witness becomes the only thing holding the value up
- 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
- 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
- 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
- quorum-types — Distributed generalization of warp-types — split-brain unrepresentable at compile time