One Rule, Three Layers: How a Shen Type Becomes Both a Compiler Check and a Runtime Guard

Most approaches to correctness give you one thing. Tests give you runtime checks against specific cases. TypeScript gives you compile-time structural constraints. Coq gives you deductive proofs. You pick your tool, you get your layer, and you accept that the others are someone else’s problem.

What I find genuinely interesting about the Shen-Backpressure approach is that a single declaration, one rule written in Shen’s sequent calculus, produces enforcement at all three layers simultaneously. The deductive layer, the compile-time layer, and the runtime layer all emerge from the same source. This is not because someone built an elaborate framework to connect them. It is because the approach exploits a structural coincidence: the same information that constitutes a proof rule also constitutes a type definition also constitutes a validation check. I want to trace through exactly how this works, show what it looks like across the most interesting domains I have found, and be honest about where the approach has sharp edges.

The Three Layers from One Rule

Consider a simple rule from a payment system:

(datatype amount
  X : number;
  (>= X 0) : verified;
  ====================
  X : amount;)

This reads: if X is a number, and X >= 0 is verified, then X is an amount. Three things happen to this declaration:

Layer 1: Deductive verification. Shen’s own type checker (shen tc+) verifies that this rule is internally consistent as a sequent calculus judgment. If I write contradictory rules, or rules that cannot compose, Shen catches this before any code is generated. This layer exists in the space of pure logic. It does not know about Go or TypeScript or any target language.

Layer 2: Compile-time structural enforcement. Shengen, the code generator, reads this rule and emits a Go struct with an unexported field:

type Amount struct{ v float64 }

func NewAmount(x float64) (Amount, error) {
    if !(x >= 0) {
        return Amount{}, fmt.Errorf("x must be >= 0: %v", x)
    }
    return Amount{v: x}, nil
}

func (t Amount) Val() float64 { return t.v }

The lowercase v is unexported. Code outside the shenguard package cannot write Amount{v: -5}. The Go compiler rejects it. This is not a runtime check and not a lint warning. It is a hard refusal to produce a binary. The constructor is the only path to the type, and the constructor’s return type (Amount, error) forces the caller to handle the failure case. The compile-time layer comes from Go’s own type system, recruited into service of the Shen spec.

Layer 3: Runtime validation. Inside the constructor, if !(x >= 0) is a runtime check. When someone calls NewAmount(-5), they get an error value back. This is the familiar validation pattern, but it is not hand-written. It is generated from the (>= X 0) : verified premise in the Shen rule. The runtime check is the same information as the deductive premise, expressed in a different medium.

One rule. Three enforcement mechanisms. No other approach I am aware of gives you all three from a single declaration. Coq and Lean give you layer 1 but not layers 2-3 in mainstream languages. Tests give you layer 3 but not layers 1-2. TypeScript branded types give you a weak version of layer 2 but not layers 1 or 3. The structural coincidence that makes this possible is that Shen’s sequent-calculus rules contain exactly the information needed for all three: the premises define the type shape (layer 2), the side conditions define the validation logic (layer 3), and the rule structure defines the proof (layer 1).

Where It Gets Interesting: Composition

Simple wrappers like amount are useful but not especially surprising. The approach becomes genuinely powerful when rules compose, because composition creates enforcement that is purely structural, with no runtime check at all.

(datatype safe-transfer
  Tx : transaction;
  Check : balance-checked;
  =============================
  [Tx Check] : safe-transfer;)

This rule has no verified premises. There is no arithmetic check, no string comparison, no validation logic whatsoever. The generated constructor is infallible:

func NewSafeTransfer(tx Transaction, check BalanceChecked) SafeTransfer {
    return SafeTransfer{tx: tx, check: check}
}

Yet this type is profoundly safe. You cannot construct a SafeTransfer without a BalanceChecked, and you cannot construct a BalanceChecked without proving bal >= tx.amount. The safety is entirely compile-time. The runtime checks happened earlier in the chain, at the leaf types. The composition is free, both in performance and in enforcement effort.

This is the pattern that I think deserves the most attention: proof chains where the interior nodes carry no runtime cost. The runtime validation happens once, at construction of the leaf types. Everything above that is pure structural enforcement by the compiler. You get the safety of dependent types with the runtime cost of a few comparisons at the boundary.

The Demo Landscape

I have been building demos to stress-test this approach across different domains, and the results are instructive because different domains exercise different aspects of the enforcement mechanism. Some of these are fully implemented. Some are specifications waiting for implementations. I will walk through the most interesting ones and flag what still needs to be built.

The Grounded Research Pipeline

The shen-web-tools demo builds a research pipeline where an AI searches the web, fetches pages, and generates summaries. The key invariant is grounding: the AI cannot cite a source it did not actually retrieve.

(datatype grounded-source
  Page : fetched-page;
  Hit : search-hit;
  (= (head Page) (head (tail Hit))) : verified;
  ===============================================
  [Page Hit] : grounded-source;)

The (= (head Page) (head (tail Hit))) premise is doing something subtle. head Page extracts the URL from a fetched page (which is [Url Content Timestamp]). head (tail Hit) extracts the URL from a search hit (which is [Title Url Snippet]). The verified premise asserts these are the same URL. You cannot construct a grounded-source by pairing a fetched page with an unrelated search hit. The URL match is checked at runtime in the constructor. The structural requirement that you have a grounded-source before you can produce a research-summary is checked at compile time.

This is the pattern in its purest form: the runtime check (URL equality) happens at one specific point, and then the compile-time guarantee (cannot produce ungrounded output) propagates through the rest of the system for free.

The same demo includes a pipeline state machine with five stages:

(datatype pipeline-idle     ...)
(datatype pipeline-searching ...)
(datatype pipeline-fetching  ...)
(datatype pipeline-generating ...)
(datatype pipeline-complete  ...)

Each stage type carries the outputs of its predecessor. You cannot skip from idle to generating because pipeline-generating requires a (list fetched-page) that can only come from pipeline-fetching. The state machine is enforced by the type system. There is no enum with a match statement. There is no “invalid state transition” runtime error. The invalid transition is a type error.

The Dosage Calculator: Recursive Type-Level Computation

Most Shen type rules use simple arithmetic: >=, <=, =. The dosage calculator demo pushes further. Its interaction-clearance type invokes Shen functions defined within the spec itself:

(define pair-in-list?
  _ _ [] -> false
  D1 D2 [[D1 D2] | _] -> true
  D1 D2 [[D2 D1] | _] -> true
  D1 D2 [_ | Rest] -> (pair-in-list? D1 D2 Rest))

(define drug-clear-of-list?
  _ [] _ -> true
  Drug [Med | Rest] Pairs ->
    (and (not (pair-in-list? Drug Med Pairs))
         (drug-clear-of-list? Drug Rest Pairs)))

(datatype interaction-clearance
  Drug : drug-name;
  Meds : (list drug-name);
  Pairs : (list (list drug-name));
  (drug-clear-of-list? Drug Meds Pairs) : verified;
  ====================================================
  [Drug Meds Pairs] : interaction-clearance;)

This is striking because the type-level proof includes recursive list-walking. It is not just “is X >= 0?” It is “walk the entire contraindication list and verify that no forbidden pair exists.” Shen’s type checker, which is itself a Prolog program, executes this computation as part of type checking. The generated Go constructor translates the recursive walk into an iterative helper function.

The final safe-administration type requires both dose-in-range (the dosage falls within the therapeutic range for this patient’s weight) and interaction-clearance (no contraindicated drug interactions). Both proofs must exist before you can administer. The composition is compile-time. The individual checks are runtime.

Multi-Tenant Authorization: The Proof Chain as Security Architecture

The multi-tenant demo has the longest proof chain: seven types, each requiring its predecessor. I have written about this one in detail elsewhere, but the key observation for this piece is how different links in the chain exercise different enforcement mechanisms:

• JwtToken and TokenExpiry are constrained wrappers (runtime validation of non-empty string, timestamp comparison)
• AuthenticatedUser is a pure composite (no runtime check, purely structural, requires the two proofs above)
• AuthenticatedPrincipal is a sum type (Go interface with private marker method, compile-time closed set)
• TenantAccess and ResourceAccess are guarded composites (runtime boolean check + structural requirement for the proofs above)

A single proof chain exercises four of the six shengen categories. The runtime checks happen at the leaves and at the boolean gates. The structural composition in between is free. The sum type is enforced by Go’s interface mechanism. This is the demo that best illustrates how the three layers interact in a real system.

Email Campaigns: Relational Invariants Across Types

The email demo has the most unusual arithmetic constraint I have encountered in any of the specs: (= 0 (shen.mod X 10)) on age-decade. This does not just require a number in a range. It requires the number to be a valid decade (10, 20, 30, …, 100). The modular arithmetic is checked at runtime in the constructor.

But the more interesting invariant is relational. The copy-delivery type asserts that the demographics embedded in a user profile match the demographics the email copy was written for:

(datatype copy-delivery
  Profile : known-profile;
  Copy : copy-content;
  (= (tail (tail (head Profile))) (tail Copy)) : verified;
  =========================================================
  [Profile Copy] : copy-delivery;)

This navigates the internal structure of two different composite types via head and tail, extracts specific fields, and asserts equality between them. It is the only demo where a verified premise compares subfields of two different composite types rather than comparing a field to a constant or to another field of the same type. This matters because it shows the approach can enforce relational constraints, properties that span multiple objects, not just local constraints on a single object.

Closed Enumerations: Rejecting LLM Hallucination

The Medicare subdomain of shen-web-tools contains what I think is the most directly practical pattern for AI-assisted development: closed enumerations.

(datatype medicare-plan-type
  X : string;
  (element? X ["original" "advantage" "part-d" "supplement" "part-a" "part-b"]) : verified;
  ========================================================================================
  X : medicare-plan-type;)

The element? check compiles to map[string]bool{...}[val] in Go, new Set([...]).has(val) in TypeScript, [...].contains(&val) in Rust. If an LLM generates a plan type of "premium" or "gold tier" or any other hallucinated string, the constructor rejects it. The closed set is enforced at runtime, and the opaque type prevents bypass at compile time.

The same spec has a panel-kind enumeration with 15 valid values for dashboard panel types. When an LLM generates a UI layout, every panel must have a valid kind. Hallucinated panel types are rejected at the guard boundary. This is backpressure applied directly to LLM output quality.

Order State Machine: Deadlock Freedom as a Type Error

This is the demo I am most excited about that does not yet exist. The concept: encode a state machine’s valid transitions in the Shen type system such that invalid transitions are compile errors and deadlock freedom (every non-terminal state has at least one outward transition) is a property of the spec itself.

The idea is that each state is a type, and each transition is a function whose type signature encodes the source and destination states:

(datatype order-created   ...)
(datatype order-paid      ...)
(datatype order-shipped   ...)
(datatype order-delivered  ...)  \\ terminal
(datatype order-cancelled  ...)  \\ terminal

(datatype transition-pay
  Order : order-created;
  Payment : payment-info;
  (> (head Payment) 0) : verified;
  =================================
  [Order Payment] : order-paid;)

(datatype transition-ship
  Order : order-paid;
  Tracking : tracking-number;
  ============================
  [Order Tracking] : order-shipped;)

The transition-pay function requires an order-created and produces an order-paid. You cannot ship an order that has not been paid because transition-ship requires order-paid, not order-created. The state machine is the type system. Invalid transitions are not runtime errors; they are compile errors.

Deadlock freedom comes from the spec structure: if every non-terminal state appears as a premise in at least one transition rule, then every non-terminal state has at least one valid outward transition. Shen’s type checker can verify this property.

Sum Types: Multiple Valid Paths to the Same Proof

The multi-tenant demo uses sum types for AuthenticatedPrincipal: both HumanPrincipal and ServicePrincipal produce the same interface type. In Go, this becomes an interface with a private marker method. In Rust, a sealed trait. In TypeScript, a union type.

What makes this interesting for the three-layer story is that the sum type adds a fourth enforcement mechanism: the closed variant set. In Go, the private marker method isAuthenticatedPrincipal() means external packages cannot add new variants. The compiler enforces the closed set at compile time. You cannot introduce a BotPrincipal without modifying the shenguard package, which is generated and audited by Gate 5.

The Category System: Six Patterns, Six Enforcement Profiles

Shengen classifies every Shen datatype rule into one of six categories, and each category has a distinct enforcement profile. Understanding these categories is the key to understanding what you get from a given rule.

The pattern I want to highlight: composite types have zero runtime cost. They are pure structural enforcement. This means that in a proof chain, the intermediate composition steps are free. Only the leaf types (constrained, guarded) carry runtime validation cost. The deeper your proof chain, the better the ratio of compile-time to runtime enforcement.

The Killer Insight: Proof Chains Have Diminishing Runtime Cost

Here is what I think is the most underappreciated aspect of this approach. Consider a proof chain of depth N:

leaf-type-1 (runtime check)
  └─> intermediate-1 (compile-time only)
       └─> intermediate-2 (compile-time only)
            └─> ... (compile-time only)
                 └─> final-proof (compile-time only)

The runtime cost is O(leaves), not O(depth). Every intermediate composition step is a composite with an infallible constructor. The compiler enforces the chain; the runtime validates the inputs. As your invariants get more sophisticated and your proof chains get deeper, the proportion of enforcement that is compile-time increases. You pay for validation at the boundary and get structural guarantees throughout the interior for free.

This is the opposite of how runtime validation typically scales. In a conventional system, deeper validation logic means more runtime checks, more error handling, more test cases. Here, deeper proof chains mean more compile-time enforcement and proportionally less runtime work. The formal properties scale by recruiting the compiler, not by adding code.

What Still Needs to Be Built

I want to be explicit about the gap between what exists as working code and what exists only as specifications or concepts, because I think intellectual honesty about the state of a project is more valuable than presenting everything as equally complete.

Fully implemented and working:

• Payment processor (Go) - simple but complete proof chain
• Multi-tenant API (Go) - full seven-type chain, tests, middleware, admin dashboard
• Email campaigns (Go) - relational cross-type constraints, working handlers and templates
• Research pipeline (Common Lisp/Shen) - the most architecturally complete, runs on SBCL

Spec complete, implementation needed:

• Dosage calculator - the spec with recursive Shen functions exists, the Go server is a stub
• Order state machine - only a concept document, the most ambitious planned demo

Concept only:

• Shen Prolog as active constraint solver for generative UI
• Linear logic / graded modalities for provable concurrency in Go
• Polyglot comparison: same spec, four frameworks (Hono, Axum, FastAPI, net/http)

The Deeper Question

I have been circling around a question that I think is more important than any specific demo: why does this work? Why can a single declaration in a proof calculus produce enforcement at three different layers of the software stack?

I think the answer has to do with the structure of sequent calculus itself. A sequent calculus rule is simultaneously:

1. A logical judgment (the premises entail the conclusion)
2. A type definition (the premises are the fields, the conclusion is the type)
3. A validation specification (the side conditions are the checks)

These are not three different interpretations bolted together by clever engineering. They are three facets of the same mathematical object. The Curry-Howard correspondence tells us that proofs are programs and types are propositions. Shen’s sequent calculus sits at the nexus where this correspondence becomes practically useful: the proof is the type is the validation. Shengen just mechanically separates the facets into their target-language representations.

This is why I think the approach has legs beyond the specific demos I have built. Any domain where you can express invariants as sequent calculus rules gets all three layers of enforcement automatically. The question is not “can we make this work for domain X” but “can we express domain X’s invariants in this notation?” And Shen’s type system, being Turing-complete and embedding Prolog, turns out to be more expressive than you might expect from a system that looks, at first glance, like simple type declarations.