For a single-language Rust project with a handful of invariants, not much. Rust's newtypes + private fields + Result-returning constructors are exactly the right primitives, and they're strictly stronger than Go's (no reflection escape hatch, no zero values to forge, exhaustive matching).
Where shengen might be more interesting:
1. Multi-language emit. If your invariants live in a Rust service AND a TypeScript frontend (or another backend), one Shen spec drives both and the build catches drift. Hand-rolled means writing the same smart constructor twice in two languages with no mechanism to keep them in lockstep.
2. Spec as the audit surface. The Shen rule for `tenant-access` is going to be much more expressive / concise than the rust implementation. The `tcb-audit` gate fails the build if generated code is hand-edited away from the spec, so reviewers read the spec and the build polices the implementation against it. With hand-rolled Rust you're reviewing the impl directly — which isn't strictly bad, but it does potentially insert the human back into the loop between LLM iterations.
3. AI in the loop. If you're hand-writing the constructors carefully yourself, the argument for shengen is fairly weak. If an LLM is writing them, "declarative spec + codegen" is, in my experience, a stronger prompt than "describe the constructor in precise English." That's the frame the post is really written for; the Rust newtype point is well-taken outside it.
I'm not saying everyone writing software (w/ LLMs or not) needs shengen / shen-backpressure. The underlying principles it's trying to help you use aren't new at all. But, if you want to get more out of LLMs (esp. multi-turn loops), you probably need something that is deterministic and structured to provide that backpressure context you want to the LLM as it iterates.
But, for everyone else: even if you skipped the sidecar entirely, didn't use the codegen, you just had the AI interpret the spec'd application into a short Shen proof, iterate until it's internally consistent / compiles...now you have a spec that is internally consistent, straightforward for human to understand, and much stronger context for the LLM than English language spec alone.
I think you're right on the substance. A production-grade spec (or guard type) needs stronger assertions than the toy example in the post — predicates for signature verification, claim-binding, and expiry-from-token, at minimum. The example is only illustrating the proof-chain shape, and isn't a good example of a full-fledged JWT validator.
Your underlying point, that calling the constructor is the assertion so AI passing `true` can "prove" whatever — is true of any smart-constructor pattern, including your own `newUnverified` approach. The trust still has to live somewhere. In your pattern it lives in the small set of audited callers; in shengen's case it lives in the same place — the wrappers (like `CheckTenantAccess`) that actually establish the premise via a DB query or a JWT parse. Structurally the two approaches are doing the same thing. To harden it, you'd keep the raw constructors package-private and export only the wrappers, so the handler code the LLM is writing physically cannot call NewTenantAccess(..., true) — only CheckTenantAccess.
On the deeper question about "why codegen": the short answer is "obviously, you don't have to." But if we assume that we're using AI to write at least some of the code, now you have to either (1) describe the constructor in very precise English and have the LLM generate it, (2) inject yourself into the loop closely with the LLM, or (3) not use an LLM for this part. My proposition is that writing the core invariants as proofs that can be deterministically checked for internal consistency and written declaratively is (1) more efficient, (2) less lossy, and (3) easier for the developer to read and reason about than writing the constructor from scratch. This puts a lot of trust in the codegen, as you point out; but as a practical matter, having a formal representation of what you want plus an English prompt is stronger context to the LLM anyway.
The other reason I started down this path, which I didn't get into in the post because I haven't figured out yet if it's truly practical, comes from a property specific to Shen: it has a very small kernel that has been ported into a lot of runtimes — Lisp, C, JS, Go, Python, Erlang, Scheme, Java, etc (https://shen-language.github.io/#downloads). That opens up the possibility of writing specs whose predicates run as runtime gates from the same Shen expression, no translation step — and even mixing compile-time and runtime assertions into the same spec. I find this very interesting conceptually, but I'm not sure yet whether it's practically useful for anything.
Author here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-Backpressure. Builds a lot on Geoff Huntley's backpressure idea -- none of this is rocket science, just an effort to apply sound programming principles in a world of LLM coding agents.
This is great but keep in mind that Go allows the programmer skip these invariants in various ways.
I wish Go had a serious type system. Never mind algebraic types, but one that fucking respected private values and did things like validating enum values.
TBH something like this sounds useful even without LLMs (although I haven't fully grokked this yet). The problem with the operational level is that you can't express the invariants etc at the type level - not least because you're working across multiple languages - so the kind of dumb issues that we're beginning to rule out at the level of the language at the process level still require lots of diligence in operational code. Some kind of shared "operational type system" that could be integrated into relevant languages would potentially help a lot.
Shen has some really unique properties that are under-developed here. It's type system itself is Turing complete and very flexible / expressive. Also, the Shen kernel is extremely compact, and easy to port into a wide variety of runtime languages (C, Lisp, Ruby, Python, JS, Go, etc https://shen-language.github.io/#downloads). What I discussed about using it as a compile-time gate + codegen is just scratching the surface, I think.
Now, a lot of the ports haven't been maintained. But the underlying Shen kernel is only 4-5k lines of code...remains extremely portable. More discussion here https://news.ycombinator.com/item?id=39602472
I didn't focus a ton on Shen in the blog post, because the underlying principles aren't really about the implementation. Shen is very cool tho.
That's not a good thing! A Turing complete type system means that compilation is potentially undecidable and non-terminating. The whole unintuitive mess in dependently-typed systems about "definitional" equality (loosely speaking, a notion of equalities that are 'trivially' checked as part of evaluation) is entirely about avoiding Turing-complete type checking!
I mean yes, that's a risk, and you are correct. In practice, is your spec about the shape of the app you want to build really going to be that complicated?
But I mentioned its Turing completeness as a lazy shorthand to illustrate that it is far more flexible and expressive than what people think of as a "type system". https://shenlanguage.org/OSM/Recursive.html
Thank you, interesting work. Please, clarify what is possibly a naive question - your README states that the constraints imposed by your tool are weaker than the formal verification guarantees. Why not implement the backpressure as the full formal verification barrier? Too complex to implement?
The distinction worth keeping clean is between the spec (here, written as proofs in Shen) being formally rigorous and the entire codebase being formally verified. Shen-Backpressure does the first: the spec is a sequent-calculus statement of invariants, and shengen lowers it into guard types the target compiler refuses to violate, so within the target language's type discipline you cannot construct a tenant-access (or any other witness) without discharging its premises.
It does not do the second (formally verify the entire codebase). Outside the guard types your Go or TypeScript is just code. It can panic, race, have bugs in unrelated logic, use reflection to forge values inside the guard package, get a wrong answer from the SQL query that fed the predicate, and so on. The proof ends at the projection boundary.
Why not go further? Not really "too complex to implement," in theory; it has been done before. But verifying the whole program is much higher engineering cost, and the trades-offs to do it make sense in a much narrower set of cases than what I'm trying to target: teams shipping production code with AI in the loop, in the language they already ship.
The pragmatic choice is to spend the verification budget on the small set of invariants that genuinely matter and leave the rest as ordinary code with ordinary review and tests. That is why the claim is phrased as "practically impossible to accidentally bypass, not categorically impossible to bypass." Over-claiming "verified" when the host language is unverified would be misleading.
Hi, thanks for the writeup, I wonder for the auth problem what you think about rego and OPA type solutions and their place in world in comparison to generated guards?
Definitely connected; OPA is itself a structural gate, but at runtime. The post focused on compile-time gates, but there's no reason a structural gate can't run at runtime — which means they compose rather than compete.
I didn't get into this in the post, but Shen is extremely portable and has been ported to a lot of different target runtimes (Go, C, Lisp, JS, many others — https://shen-language.github.io/#downloads). But, OPA offers extremely fast runtime execution in a way that would be more difficult to get to in Shen. What the compile-time guard adds is that it can make the runtime invocation non-skippable — so you could have a compile-time assertion that the code calls the runtime assertion, with OPA sitting behind the constructor. The catch is that if you still want all your invariants in Shen but use OPA for the runtime layer, that's another translation layer to keep in sync (Shen → Rego alongside Shen → guards). The alternative is to lean on Shen's portability: you could run the same spec at runtime with no translation layer at all, trading OPA's speed for that simplicity. Either way they're similar concepts run at different times. Integrating both into one high-level spec is mostly a question of which of those tradeoffs you want.
And, given need to allow for errors in estimation and eventual deterioration of many alpha-generating strategies, adjusting investment fraction downward (a sort Bayesian prior, I suppose) is sensible on its own, sans vol sensitivity considerations.
This is also an argument for finding investments that allow you to better define the downside risk of investments. I think that this is why static investments or hedges have such value; they may not change the expected value, they might even reduce it (based on mean estimates), but they reduce / eliminate the estimation error in your downside risk, allowing you a much more certain calculation of leverage.
Most of the examples of Kelly criterion application are either concrete bets with discrete payoff/loss odds and values, or assumed to be normally distributed. This paper discusses how extremely skewed outcomes (eg, stock options) should affect the Kelly calculation: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=2956161
The reasoning behind the Kelly Criterion was explored recently in a more broad context, showing that the logarithmic utility is not required: https://aip.scitation.org/doi/10.1063/1.4940236
Where shengen might be more interesting:
1. Multi-language emit. If your invariants live in a Rust service AND a TypeScript frontend (or another backend), one Shen spec drives both and the build catches drift. Hand-rolled means writing the same smart constructor twice in two languages with no mechanism to keep them in lockstep.
2. Spec as the audit surface. The Shen rule for `tenant-access` is going to be much more expressive / concise than the rust implementation. The `tcb-audit` gate fails the build if generated code is hand-edited away from the spec, so reviewers read the spec and the build polices the implementation against it. With hand-rolled Rust you're reviewing the impl directly — which isn't strictly bad, but it does potentially insert the human back into the loop between LLM iterations.
3. AI in the loop. If you're hand-writing the constructors carefully yourself, the argument for shengen is fairly weak. If an LLM is writing them, "declarative spec + codegen" is, in my experience, a stronger prompt than "describe the constructor in precise English." That's the frame the post is really written for; the Rust newtype point is well-taken outside it.
I'm not saying everyone writing software (w/ LLMs or not) needs shengen / shen-backpressure. The underlying principles it's trying to help you use aren't new at all. But, if you want to get more out of LLMs (esp. multi-turn loops), you probably need something that is deterministic and structured to provide that backpressure context you want to the LLM as it iterates.
reply