A new preprint proposes a software model designed to make runtime changes easier to reverse and dependencies easier to manage as components come and go. Its central question is how dynamic software composition can support reversible side effects while reacting to changing links between components.
The work does not use a participant sample or a controlled comparison. Instead, it develops a formal calculus, theorem statements, operational rules and algorithms, then describes an implementation called Cordis and a qualitative case study in the Koishi software ecosystem. The main results are therefore formal and conditional, while the applied evidence is observational.
A framework for runtime change
The framework lifts effects and coeffects into runtime mechanisms. In ordinary terms, it treats the changes a component makes and the dependencies it requires as part of the runtime account of composition. A unified context carries both kinds of information and mediates every interaction, while independence between components is judged by what an observer can distinguish.
For changes over time, the revertible-effects construction pairs every tracked effect with an inverse and records how those inverse actions compose. When a component is removed, the calculus can apply the composed inverse actions associated with its activity. The result is a formal local temporal-composability property, and it depends on the inverse witnesses and on the paper's chosen boundary for what counts as observable.
Dependencies are handled as a live condition rather than a one-time lookup. Reactive coeffects declare what a component needs, classify each context change as activating, deactivating or neutral, and use that classification to drive lifecycle transitions. The global ordering rule keeps a provider's binding available until every dependent that resolved it has deactivated. During an activation episode, all iterations use one committed dependency resolution, so the transition does not switch targets halfway through.
What the formal results claim
The paper also addresses interleaving, the case in which separately tracked component actions are mixed together. Its recovery-exactness result says that applying one component's accumulated inverse after that interleaving leaves the other components' table effects where the same intervening steps would have left them, up to the stated observational equivalence. The comparison excludes control fields, and the result is not a promise of byte-for-byte restoration of every physical side effect.
Two further theorems set conditions on lifecycle behavior. Under assumptions including acyclic dependencies, bounded iterator length, finite names and lifecycle-only steps, the progress result says every maximal lifecycle sequence ends in a quiescent state. The confluence result says that runs with the same orchestration inputs reach states equivalent up to renaming and the paper's observational relation, subject to its provision-totality and quiescence assumptions and excluding failed fibers.
From formal rules to a working ecosystem
Cordis translates those ideas into a runtime package. Its core library handles effect tracking and coeffect resolution, while a declarative loader reconciles configuration and supports hot module replacement. The supplied analysis reports no quantitative overhead or baseline comparison.
The case study's practical anchor is Koishi, a production software ecosystem that the paper reports as having over 4,000 community plugins. The authors present this as evidence that the abstraction exists in use and has been adopted in that setting, not as a quantitative evaluation. Because the evidence comes from one ecosystem and one host language, it cannot by itself separate the framework from that particular implementation and domain.
Cordis does not verify that the inverse witnesses supplied by component authors are correct or that the commutativity witness used for dependency changes is valid. The formal conclusions are therefore conditional on those obligations and on the assumptions of the calculus.
Taken together, the work offers a formal foundation for reversible effects and reactive dependency management, plus an implementation and one adoption example. It does not supply a controlled test of competing architectures or a measure of performance, so its strongest contribution is a set of conditional rules for dynamic composition rather than a demonstrated universal solution.
Paper data and sources
Original title: A Programming Paradigm for Spatiotemporal Composability
Authors: Yifan Shi, Wei Zhang, Tianyi Cui
Journal/Repository: arXiv
Status: Preprint, not yet peer-reviewed
First online: 2026-08-26
DOI: Not available
Original paper · Full text