A Programming Paradigm for Spatiotemporal Composability
https://github.com/cordiverse/paper
1. 论文身份: DeepSeek背后的论文支撑，作者来自北京大学与 DeepSeek，理论落在开源元框架 Cordis 上；DeepSeek 开源的 DSH 在仓库文档中声明由 Cordis 驱动。
2. 核心问题: 运行时动态组合（加载、卸载、替换组件）长期缺少形式化基础，论文把它拆成时间可组合性（卸载后副作用完整回收）与空间可组合性（依赖声明与响应式管理）两个正交维度。
3. 方法一句话: 把程序语言理论里的效应与余效应从编译期静态分析改造成运行时机制——每次环境修改自带逆变换（可逆效应），每份依赖写成声明式规格并随上下文变化分类响应（响应式余效应）。
4. 关键机制一: 逆变换由调用方在执行点当场构造并满足见证约束，运行时把各步逆变换按相反顺序复合成后进先出的累加器，组件卸载即调用累加器把环境还原到加载前。
5. 关键机制二: 提供者卸载分两阶段，先让服务对外不可见、等所有消费者完成清理，再执行累加器释放资源；加载按效应迭代分步推进，目标变化在迭代边界分流卸载，在途异步操作落地后即转卸载，失败回滚并记录在组件实例上。
6. 形式化保证: 保持性、恢复精确性、保序性、进度、合流性五条元定理，分别依赖良构注册表、操作两两独立、依赖无环且迭代有界、无失败且静止等明确前提；合流性明确不覆盖失败情形。
7. 观测等价: 恢复是"外部观察者无法区分"意义的等价，不是字节级还原，由此内存分配布局、生成性名称等实现差异被吸收，多组件交错修改下的效应独立性才成立。
8. 实现与案例: Cordis 用单原语 ctx.effect 跟踪全部上下文修改，插件作者无需另写卸载路径；事务式热模块替换导入失败可整体回滚；Koishi 生态四年积累四千多个社区插件，属单一 TypeScript 生态观察性案例而非受控对比。
9. 系列定位: Meta-Harness、AHE、Continual Harness 回答 harness 能否被自动搜索与演化，Autogenesis 给出协议层直觉，本篇回答每一次热替换的正确性由什么保证，可视为 harness 自动优化系列的形式化地基篇。
10. 边界判断: 发射型操作（写共享文件、发网络数据）不可恢复，只能靠延迟提交或应用层补偿；键的可交换性是提供者接口义务；暂无抽象开销的定量数据；不可信代码仍需外部沙箱。
