> series
shen-backpressure
Posts in this series, in reading order. New entries added as they’re ready.
- [01] The Abstraction Ladder Has Always Been ThereA spec isn't an alternative to code — it's code at a different level of abstraction. The decisions you don't make get made for you.
- [02] The Spec Is Not a Gate, It Is a SubstrateFour places one .shen file can enforce itself — and why that changes what a specification is for.
- [03] The Spec Is the Oracle, Not the GeneratorAn inversion buried in the shen-derive pivot that generalizes to almost every verified-code project.
- [04] One Rule, Three Layers: How a Shen Type Becomes Both a Compiler Check and a Runtime GuardA single sequent-calculus rule produces deductive, compile-time, and runtime enforcement — not by bolting layers together, but by exploiting a structural coincidence.
- [05] One Spec, Five Languages, Five Different GuaranteesThe strength of a compile-time invariant is bounded by the weakest link in the enforcement chain — and different languages provide very different enforcement substrates.
- [06] From Sequent Calculus to Guard Types: How Shengen WorksSix patterns classify every Shen datatype rule, and each generates different code. A tour of the codegen taxonomy and the hidden structure of the validation problem.
- [07] The LLM Does Not Know It Is Being Formally VerifiedBehavioral constraints degrade under autonomy; structural ones do not. You do not need smarter models — you need smarter types.