[d] Long-term: "obleeny" — maximal principal reduction → provable inertness

[hyperpolymath]

The longer-term research / architecture horizon (scope d).

Vision

Reduce each cartridge to its minimal essential computational core — exactly the capability it needs and nothing more — so it is "utterly inert but for what it is supposed to do," and therefore provably very hard to misuse.

Directions to explore

• Capability-typed algebra (tagless-final, Oleg-Kiselyov-flavoured): a cartridge is a typed term over an effect/capability algebra; its type names exactly its capabilities and the harness denies the rest by construction (least authority).
• Maximal principled reduction: partial evaluation / normalisation of a cartridge to a minimal core; dead-capability elimination as a typed property.
• Trusted-base → 0: discharge the 5 core axioms (scope a, [proofs/a] boj-server core: enforce + minimise the trusted base #197) constructively; aim at a cartridge whose only trust is the Idris kernel.

Connects to

• The maker (scope f) must emit capability-minimal artifacts by construction and must not foreclose this path.
• The base proof bundle (scope c, [proofs/c] Special/base cartridges (cross-cutting: agentic · nesy · orchestration · fleet · build · debug · health) boj-server-cartridges#37).

Note on the name

I've read "obleeny … maximal principal reduction" as the Oleg-style principled-reduction idea (tagless-final + partial evaluation toward a minimal, least-authority core). Please confirm if you meant a specific person/system so the references aim correctly.

Not blocking near-term — but the proofs + maker should be designed so this stays reachable.

---

Filed via Claude Code · https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa