2026-08-15Tao
How Software Components Can Be Plugged In and Pulled Out Safely
This 88-page preprint splits dynamic software composition into temporal and spatial problems, then uses revertible effects, reactive dependencies, and a unified context to explain safe loading, unloading, and rewiring at runtime.
Contents13 sections
- Why a plugin is so hard to remove cleanly
- Time and space are different problems
- Revertible effects give every operation a cleanup receipt
- Reactive environmental dependencies follow service changes
- Context is the system's shared ledger
- Four lifecycle states account for asynchrony and failure
- What the paper proves
- Which premises make those proofs work
- How Cordis puts the theory into code
- Koishi offers a real sample and a clear evidence boundary
- Security boundaries still need separate treatment
- Why self-evolving agents may need this model
- Safe removal completes the idea of dynamic composition
Original paper: A Programming Paradigm for Spatiotemporal Composability
Preprint draft dated 2026/8/13 · 88 pages · Authors: Yifan Shi, Wei Zhang, and Tianyi Cui
Affiliations: Peking University and DeepSeek-AI · Implementation: Cordis · Case study: Koishi
The paper repository explicitly describes the preprint as an active revision whose contents may change substantially.
Installing a software component is usually easy. Removing it completely is much harder.
A plugin can register event listeners, timers, and routes, open ports, establish database connections, and publish services to other plugins. Missing one cleanup step leaves the process running with residual state. Restarting the process is the simplest escape because the operating system reclaims everything at once.
That restart also discards caches, connections, and work in progress. The whole process pays for one plugin's problem.
A Programming Paradigm for Spatiotemporal Composability tries to turn this engineering habit into a programming model that can be described, implemented, and proved. It asks two questions: Can a component completely withdraw the changes it made, and can the system automatically coordinate components when their required services appear, disappear, or change identity?
The paper calls the first property temporal composability and the second spatial composability. Together, they form spatiotemporal composability.
Why a plugin is so hard to remove cleanly
The paper uses the Visual Studio Code extension system to illustrate the limits of current practice.
In the authors' analysis, VS Code extensions share an extension host process. An extension can be installed dynamically, yet code and effects left by an executed activate function cannot be fully removed from that same process. Disabling or uninstalling an extension requires restarting the extension host, while deactivate behaves more like a shutdown cleanup hook.
The paper also surveyed the 100 most installed extensions on 2026/6/9. Only 7 declared a dependency on a non-built-in extension through extensionDependencies. This is an author-collected marketplace statistic that helps characterize the example. It is not an independent benchmark for plugin systems as a whole.
Plugin platforms often keep extensions inside a fixed menu of host-defined commands, views, and language features. When extensions need to cooperate directly, their dependency relationships tend to move into runtime code with weak typing and lifecycle constraints.
Processes and containers provide a coarse answer. The operating system reclaims memory, file descriptors, and ports when a process exits. A container orchestrator can restart services according to service-level dependencies. Neither mechanism directly expresses ownership and dependency relationships among dozens of components sharing one address space.
The paper works one level lower: remove only the component that must leave while the rest of the process keeps running.
Time and space are different problems
Temporal composability asks what a component leaves behind.
Loading a component changes a shared environment, and unloading it must withdraw those changes. Listeners must be detached, timers stopped, ports closed, child components retired, and registry entries removed. Order matters. A resource created later often relies on one created earlier, so cleanup commonly runs in reverse order.
Spatial composability asks what a component needs.
A business plugin may require a database service and a messaging adapter. It should remain inactive while the database is missing. When the database provider is replaced, the plugin must stop using the old instance, complete cleanup, and then connect to the new instance. A database provider that is leaving must wait until its consumers have finished.
Static programs resolve module imports before execution, and lexical scopes delimit many resource lifetimes. Components in a dynamic system arrive and depart at runtime. Both the dependency graph and resource lifetimes keep changing, so static boundaries are insufficient.
Revertible effects give every operation a cleanup receipt
The paper adds a runtime obligation to an effect. An effect returns a new state together with a function that can withdraw the change.
Its simplified shape is:
current context -> new context + recovery function
Registering a listener returns a function that removes it. Opening a server returns a function that closes it. Overwriting configuration returns a function that remembers and restores the previous value.
The recovery function can depend on the state at the exact point where the operation ran. The old configuration value is available only then. Each cleanup receipt therefore captures the information required for that particular application.
The runtime collects these functions as the component executes. If a component performs A, B, and C, cleanup runs C, B, and A. This last-in, first-out order preserves nested resource relationships naturally.
The component author supplies recovery for atomic operations, and the runtime derives recovery for their composition.
The paper calls these structures revertible effects. They are easier to audit than a separate deactivate procedure because acquisition and recovery stay together, and the runtime knows which component owns each effect.
Reactive environmental dependencies follow service changes
The second half comes from coeffects. An effect describes what a program does to its environment. A coeffect describes what the program requires from that environment.
The paper stores dependencies in a typed, keyed context. A component first declares the keys it requires, such as database, router, or logger. The runtime checks whether active providers supply every key and classifies each mediated context change in one of three ways:
- Missing dependencies become complete, so the component begins activation.
- Complete dependencies lose a key, so the component begins deactivation.
- Satisfaction does not change, so the component remains where it is.
Dependency relationships become lifecycle inputs instead of failures discovered on first access.
When a database component leaves, the runtime first makes it unavailable to new consumers. Existing consumers retain the committed view they captured on activation. They can still use the old database binding during cleanup to return transactions, connections, or caches properly. The provider runs its own recovery functions only after all consumers have finished deactivation.
The provider first stops advertising service, consumers clean up next, and the provider releases resources last.
That ordering addresses a subtle dynamic dependency problem: teardown code often needs the same dependency whose removal triggered the teardown.
The paper adds two extensions. Isolation lets one dependency key resolve to different instances in different contexts, which supports multi-tenant systems, tests, and local isolation. Interception merges metadata when a dependency is accessed, which can carry path restrictions, read-only policy, or other invocation rules.
Context is the system's shared ledger
The paper eventually places effects and coeffects inside one recursive context.
Each component receives a child context. It registers resources, reads dependencies, and creates child components through that context. The parent context accumulates the effects of its children. When one child leaves, only that child's contribution is recovered. Nested components form a tree that can be loaded and unloaded one level at a time.
This context works like a partitioned ledger. Every resource has an owner, every dependency has a provider, and every change passes through one entry point. The runtime can then answer three questions: who changed the state, who depends on a service, and who must leave first.
The paper also gives recovery a practical definition. A heap may not have the identical byte layout after allocation and release. A generated name may be different the next time one is drawn. The formalism uses observational equivalence: two states count as equivalent when the operations exposed through the context cannot distinguish them.
The recovery target is therefore the same externally observable behavior, without requiring a byte-for-byte restoration of physical representation.
Four lifecycle states account for asynchrony and failure
Real component loading and unloading take time. A database connection may wait on a network. A module import may fail. A dependency may change while a component is only halfway through loading.
The paper starts with Inactive and Active, then introduces Reloading and Unloading to form a four-state lifecycle:
- Inactive: the component is not running and provides no dependencies.
- Reloading: the component is installing effects step by step.
- Active: loading has completed and the dependency view is committed.
- Unloading: the component has stopped providing service, is waiting for consumers, and is recovering resources.
An activation can be divided into iterator steps. After each step, the runtime checks whether the target dependency view still matches the one captured at the beginning. If it changed, completed steps are recovered.
An asynchronous operation already in flight is allowed to land, after which the fiber moves directly into unloading. This prevents a half-loaded component from briefly advertising service. If a step fails, the system recovers previously accumulated effects, records the error on that fiber, and leaves sibling components running.
What the paper proves
The mathematically heavy part of the 88-page paper is a calculus of dynamic composition. A component has three parts: required dependencies, dependencies it may provide, and an effect with recovery. One running instance is called a fiber, and each fiber stores its own lifecycle, committed dependency view, and accumulated recovery function.
The authors prove several families of properties over this model.
1. Structural invariants remain preserved
After any legal step, the registry remains well formed. Parent relationships remain valid, an unisolated dependency key does not have two providers, and a running consumer continues to name a provider in a valid lifecycle state.
2. A departing component withdraws only its own contribution
When operations from different components meet the independence conditions, one fiber's accumulated recovery can pass through later changes made by other fibers. It removes its own contribution while preserving theirs.
3. Consumer lifetimes fit inside provider lifetimes
A consumer begins loading only after its provider is active and finishes unloading before the provider recovers resources. The dependency resolution used by one transition also stays coherent, so the transition does not mix an old provider with a replacement.
4. The system eventually becomes quiet
When dependency precedence is acyclic, the set of fibers is finite, and each activation has a bounded number of steps, provider withdrawal cannot wait forever. Lifecycle processing reaches a quiescent state where no component needs another transition.
5. Final state does not depend on the intermediate path
Under stronger premises, independent component activations and deactivations can interleave in different ways and still produce the same quiescent state for the same final composition. The result matches one dependency-ordered assembly from scratch. The paper calls this confluence.
In engineering terms, the system remembers the composition it should end with without carrying every intermediate rearrangement forever.
Which premises make those proofs work
The formal results do not place an automatic safety shell around arbitrary JavaScript. They rely on explicit disciplines.
All shared changes must pass through the context. If a component mutates a global variable or calls an unwrapped API, the runtime cannot see or recover that effect.
Recovery functions must be correct. Cordis can collect and invoke them, but the current runtime cannot prove that one truly reverses the matching operation. The foundation API or component author still carries that responsibility.
Effects from different components need the required independence. Informally, one component's operations and recovery should not change the result or recovery behavior of another. Operations on distinct dependency keys are often independent. Ordered middleware chains, shared counters, and address allocators need additional design.
Dependency precedence must be acyclic. If A waits for B while B waits for A, both remain inactive. The paper suggests factoring bidirectional interaction into smaller core and integration components. This can increase component count and configuration complexity.
Confluence additionally excludes failed fibers and assumes components install all the keys they declare as provisions. External emissions also sit outside ordinary rollback. Closing a file descriptor can withdraw a resource acquisition. Bytes already written to a shared file, a network message already sent, or a completed charge generally cannot be erased by an ordinary inverse. Such actions need delayed commitment or application-specific compensation.
How Cordis puts the theory into code
The implementation described in the paper is Cordis. It does not target the web, databases, chatbots, or another particular domain. It supplies dynamic component composition semantics beneath those frameworks.
ctx.effect(callback) drives an effect callback and collects the recovery function yielded by each step. ctx.set and ctx.get provide and read dependencies. ctx.use creates a child component. Isolation and interception adjust the scope of resolution and the policy applied on dependency access.
The component loader turns declarative configuration into fibers. When configuration changes, it rebuilds only affected entries. Hot module replacement first backs up module caches, disposes old fibers, and imports replacements. If any import fails, it restores caches and prior components so the system does not remain half-reloaded.
The public Cordis repository describes the project as a meta-framework for spatiotemporal composability and also warns that it remains under active development with an unstable API. Cordis v4 in the paper is best read as an evolving reference implementation rather than a frozen industry standard.
Koishi offers a real sample and a clear evidence boundary
The paper studies the open-source chatbot framework Koishi. Messaging adapters, database drivers, administrative consoles, and end-user features all exist as plugins on the server. The browser console is another independent Cordis application.
The paper describes an ecosystem built over four years with more than 4000 community plugins. The official Koishi marketplace recently displayed 3952 plugins available for v4. The timing and counting semantics differ slightly, but both figures show that the model has carried a large, open plugin ecosystem.
Koishi lets an operator disable a plugin from its console and supports hot reload during development. Commands, listeners, and services registered through context are recovered when a plugin exits. Dependents react when a provider changes.
A footnote in the paper keeps the main qualification visible: Koishi currently uses Cordis v3, while the paper presents a redesigned Cordis v4. Koishi's operating history supports the compositional core shared by the two generations. It does not independently validate every new v4 semantic rule or theorem correspondence.
The authors also frame the case study as evidence of existence and adoption. It covers one ecosystem in one host language and is observational rather than a controlled comparison. Runtime overhead, recovery latency, and changes in developer productivity have not yet been measured quantitatively against a baseline.
Security boundaries still need separate treatment
Dependency declarations can restrict which services a component accesses through the context proxy. Interception can attach read-only paths, database permissions, and other policy metadata. This provides a form of capability-based access control.
Malicious code with direct access to the host runtime can bypass context. The paper assigns isolation of untrusted components to an external sandbox, such as a separate process, another language runtime, WebAssembly, or a container. Cordis manages component composition and resource ownership; it does not itself form a hostile-code sandbox.
Version compatibility across components is also incomplete. The current model links providers and consumers primarily by key identity. Independently developed plugins can collide on one key name, or an interface can change while retaining its key. Cordis currently uses npm peer dependencies to mitigate version mismatches, while structural compatibility and behavioral contracts remain open problems.
Why self-evolving agents may need this model
The paper treats self-evolving agent harnesses as an important motivation.
An agent harness can manage tools, permissions, sandboxes, memory, context, subagents, and persistent state. A future agent that rewrites its own tools and runtime modules turns every modification into a dynamic composition event. A restart interrupts tasks and loses process-local state. A direct code replacement can leave old effects behind or silently break dependent modules.
Spatiotemporal composability offers a possible foundation. An old component withdraws its contribution, a replacement activates only after its dependencies are satisfied, consumers finish cleanup before a provider leaves, and failed updates return to a stable state.
This remains future validation. The paper does not report a Cordis deployment in a continuously self-modifying agent harness. It gives a concrete reason to try and leaves the most important experiment undone.
Safe removal completes the idea of dynamic composition
The paper extends composition beyond modularization and plugin installation toward three stricter outcomes: component changes can be withdrawn, dependency changes can be coordinated, and final state can become independent of the intermediate path.
Its value comes from both the unified model and its explicit boundaries. Effects outside context do not disappear automatically. External emissions resist ordinary rollback. Incorrect recovery functions still fail. Untrusted code still needs a sandbox. Quantitative benefits remain unestablished.
Cordis demonstrates an executable implementation path, and Koishi shows that the shared core can support a real plugin ecosystem. The next tests concern Cordis v4's own performance and engineering cost, plus whether the model keeps its guarantees across other host languages, distributed systems, and self-evolving agents.
Software components have long been compared to building blocks. The paper adds the missing half of that metaphor: after a block is attached, the system must still be able to remove it safely.
- Published from
- atlasnote-editorial
- Published
- 2026-08-15
- Tags
- programming-languagessoftware-architecturepluginscordis