# An 88-Page Paper in Three Pages: Reading DeepSeek’s Cordis on Spatiotemporal Composability

This article is for readers meeting the Cordis paper for the first time. The first half asks why 88 pages is too much; the second half states the core in short form. If you only want “what does the paper actually say?”, jump to Three pages for the core.

What is an 88-page paper trying to say?

Authors affiliated with DeepSeek-AI and Peking University recently posted a preprint: A Programming Paradigm for Spatiotemporal Composability (Draft of August 13, 2026). It is the design story of Cordis, a meta-framework for safely loading, unloading, and replacing components at runtime. The repo marks it as a preprint under active revision—check the latest version before citing specifics.

My first reaction after reading: the core idea can be told in a short piece.

That is not a dismissal. There is real substance—lifting “clean unload” and “dependency tracking” into runtime mechanisms with proofs, including system-level confluence. But that substance sits inside a thick quilt of formal definitions, related work, and discussion. Most readers give up before they reach the pearl.

This post does two jobs: explain why 88 pages is heavy for first-time readers, then align the paper’s core in engineer language. It sits in the same family as Harness Engineering—how to constrain agent runtimes—and is a different cut from Harness as function composition: that piece abstracts outer orchestration; this one reads a PL/systems paper that formalizes dynamic pluggability.

Why 88 pages is too many

How simple the core actually is

The paper’s own axis is two dimensions; in engineering talk, three sentences:

1. Temporal: plugins that go on can come off; side effects roll back automatically—like GC, but for effects instead of memory.
2. Spatial: dependencies are declared and resolved; missing deps keep a component idle; arrival activates; withdrawal rolls dependents back.
3. Together: no matter the install/uninstall order, the final state matches a one-shot static assembly of the components still alive—what confluence is meant to guarantee.

An experienced engineer already hears undo logs, RAII, OSGi, and DI. The core can be told short.

Where the pages go

A rough map from the table of contents (page ranges overlap; for skimming only):

Content	Rough locus	Value for a general reader
Formal model and metatheory (incl. confluence)	§§3–4, ~30+ pages	Skip detail unless you will check proofs or follow the research
Related work (effects/coeffects, plugin/hot-reload lineages)	§7	Academic hygiene; not first-read priority
Cordis implementation and Koishi case	§5	Engineering signal; watch the v3/v4 footnote
Discussion (boundaries, sandboxing, language independence)	§6	Useful, mixed with open problems and vision
The intuition you should keep	Intro dimensions + §3 mechanism intuition + confluence statement	Everything covered in the next section

Why so long? Partly PL convention: each idea wants intuition, definition, examples, properties, and proof. Partly author choice: they want both sides—a calculus and an implementation/production story. Stack them and you get 88 pages. A pure theory cut or a pure systems cut could each be shorter.

Terminology inflation

“Twisted composition monoid” names how forward transforms compose with inverses. In engineering English, that is ordered, reversible composition. A plainer name would teach the same idea. The vocabulary is not necessarily bluffing, but it raises the bar.

The practical effect: the audience shrinks. Far fewer people will finish 88 pages of PL metatheory than could benefit from Cordis’s engineering move. A shorter alignment of the core would reach an order of magnitude more readers.

Three pages for the core

No PL background required.

The problem: plugins do not come off clean

Runtime load/unload/replace is decades old—OSGi, Spring, VSCode extensions, Erlang hot code loading—yet one pain recurs:

Easy to attach; hard to detach cleanly.

Plugins register listeners, open connections, mutate config. Unload must undo all of that. The usual bargain is hand-written cleanup in stop() / deactivate(). People are unreliable. The paper cites marketplace data: among the top 100 VSCode extensions by installs, 87 ship executable code and typically need a full extension-host restart to remove—not laziness, but side effects that are too many and too implicit to verify complete cleanup.

The paper splits the need into two dimensions:

• Temporal composability: when a component leaves, its modifications to the shared environment must be fully and safely reversed.
• Spatial composability: inter-component dependencies must be declared and discovered, with structured lifecycle coordination as those dependencies change.

A motivating horizon is the self-evolving agent harness: if a harness rewrites its own components without stopping service, fine-grained spatiotemporal composability stops being optional. Coarse substitutes (process restart, container orchestration) are costly and misaligned with in-process composition.

Cordis’s answer: two dimensions, three sentences

1. Automatic rollback (revertible effects)

Mutations of system state should go through one tracked interface (in the implementation, ctx.effect). Each mutation records its inverse:

• registered a listener → remember “unregister”
• changed a config value → remember “restore”
• opened a connection → remember “close”

On unload, the runtime runs inverses in reverse and restores the pre-load state. Authors need not hand-write a full cleanup path—provided effects go through the tracked door.

Same migration as GC removing free from your job description: GC owns memory; Cordis owns (context-mediated) effects.

2. Automatic dependency orchestration (reactive coeffects)

Each component declares what it needs. The runtime drives lifecycle from those specs:

• deps satisfied → activate
• missing deps → stay idle
• deps withdrawn → roll back the dependent’s effects, then finish unload

Independently authored plugins coordinate mainly through dependency specs. Think Spring IoC, plus reactive response when the runtime dependency topology changes—not only inject-once at boot.

3. Order-insensitive safety (confluence)

Those two pieces underwrite a key metatheoretic claim:

Whatever interleaved order you use to add, remove, or replace components, the final state should be observationally equivalent to statically assembling the finally surviving configuration.

Intermediate thrashing leaves no dirty residue—if effects really reverse and dependency changes really coordinate. Like a document you type and delete: the final text depends only on what remains, provided delete actually deletes. Cordis aims to guarantee the “actually deleted” part.

Confluence is the formal result engineers should care about most. Preservation, global temporal/spatial composability, and Progress sit beside it; order-insensitive safety is the takeaway.

Versus existing approaches

System	Effect cleanup	Dependency management	Order-safety guarantee
OSGi	Hand-written stop()	Service Registry	No formal confluence claim
Spring	Hand-written destroy()	IoC container	None
VSCode	Hand-written deactivate()	Extension deps (rarely used)	None; often restart the host
Erlang/OTP	Hand-written code_change, etc.	No same fine-grained model	No same statement
Cordis	Runtime tracking + rollback	Declarative + reactive	Calculus metatheory (incl. confluence)

The decisive column is the first: who is responsible for clean effect disposal. Legacy stacks bet on author diligence; Cordis tries to discharge that diligence into the paradigm and runtime.

What is actually valuable

Do those thirty-plus formal pages matter?

One line of argument is necessary: lifting local revertibility and reactive dependence to global properties on interleaved components—especially confluence. Dynamic composition sequences can interleave arbitrarily; engineering intuition that “it should be fine” fails on edge cases. Does load A, load B, unload A, load C end like another path? Manual reasoning errs; proofs are what can underwrite the claim.

In the Koishi case study, the paper puts the engineering point cleanly: correctness that would otherwise rest on each author’s diligence is instead discharged once, by the abstraction. Same directional move as GC shifting memory management from people to the runtime.

Without that structural guarantee, the paper’s value drops sharply; with it, “order-safe dynamic composition” has a load-bearing wall. The rest of the calculus is second priority for understanding the idea—first priority only if you will check the proof.

Real problems remain

Formal story and production evidence are misaligned

This is the sharpest critique. A footnote is explicit: Koishi currently runs Cordis v3; the paper presents Cordis v4 (refined effect/coeffect semantics and a redesigned loader). The core compositional model is shared; the systems are not identical.

You prove one narrative and validate mainly on a predecessor. Reading Koishi’s scale as “v4 theory is isomorphic-validated in production” overclaims. The paper discloses the gap in a footnote that readers easily miss.

Single ecosystem, no controlled comparisons

The main validation arena is Koishi (thousands of community plugins; server bot plus browser console, etc.)—rich, but one ecosystem and one primary language line (TypeScript). There is no head-to-head controlled comparison with OSGi, Erlang hot reload, or VSCode’s extension host. You cannot extract a crisp “how much better” number; some overhead and productivity comparisons are left as future work.

Effects outside the system boundary

Discussion admits: only locations the system can exclusively modify and restore lie inside the tracked boundary. Third-party code that bypasses ctx.effect and mutates globals or prototypes is not followed. Guarantee strength equals how many effects are willing to walk through the context door—not fine print; the model’s scope.

Vision ahead of results

Self-evolving agent harnesses are a strong motive, not a closed validation loop. Fine-grained dynamic composition matters for nonstop self-modification, but “agents rewrite their production harness” is a direction, not a product conclusion the paper has already sealed.

Advice for a first reading

1. Read the intro dimensions and motivating examples until “clean detach / dependency follow-through” clicks.
2. Read §3 for mechanism intuition (revertible effects, reactive coeffects, unified context); skip formula expansions you do not need.
3. Read the prose statement of confluence (and sibling theorems)—what is guaranteed; leave proof trees for later.
4. Read §5 on Koishi when you care about engineering feasibility; keep the v3/v4 footnote in view.
5. Skim Discussion selectively (system boundary first); skip Related Work and long proofs unless required.

Verdict: right direction, hard theory, soft validation, long form. The real contribution is not rediscovering that plugins are hard to unload; it is turning spatiotemporal composability into a runnable paradigm and attempting formal load-bearing for interleaved dynamic composition—especially confluence. Formal object and production mainline are not fully aligned; single-ecosystem evidence is thin; 88 pages is heavy for the core idea.

Worth a serious read; not suitable to cite as a closed, fully validated conclusion. If you only need “what it does and why it matters,” this section is enough; for proofs or implementation detail, open the PDF on GitHub.

References

• Shi, Zhang, Cui — A Programming Paradigm for Spatiotemporal Composability (cordiverse/paper, preprint)
• On this site: Harness Engineering, AI Harness as Function Composition