;; writing
Essays and notes. Full feeds, no tracking. Subscribe via rss or email.
> series
> posts
- 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.#shen-backpressure :1
- 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.#shen-backpressure :2
- The Spec Is the Oracle, Not the GeneratorAn inversion buried in the shen-derive pivot that generalizes to almost every verified-code project.#shen-backpressure :3
- 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.#shen-backpressure :4
- 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.#shen-backpressure :5
- 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.#shen-backpressure :6
- 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.#shen-backpressure :7