口号背后的证明

口号背后的证明

DeepSeek 的 Agent Harness 把四个词印在海报上,背后却站着一篇长长的论文。论文真正主张的东西要克制得多,也有意思得多。

阅读时长: 15 分钟

2026 年 8 月,DeepSeek 以 MIT 许可证发布了一套 Agent Harness,宣传页正中央写着四个醒目的英文单词:Everything is a Plugin(一切皆插件)。而在这句口号背后,还有一篇预印本论文——时空可组合性的编程范式

关于这次发布带给我的感受,我已经另写了一篇文章。这里想谈的是另一半:它究竟提出了什么。因为很多人和我一样,看到那句口号时,会下意识觉得自己已经知道答案了。

但口号和论文,其实是两份气质完全不同的东西。

口号描述的是软件行业从 20 世纪 90 年代起就在做的事;论文真正尝试证明的,则是一个范围小得多、但也有趣得多的命题。

并不新鲜的部分

所谓插件,就是不必拆开程序主体,也能装进去或拔出来的功能模块。

浏览器里的广告拦截器是插件,相机机身上的镜头也可以看成一种插件。这个思路一点也不新,论文作者也没有假装自己发明了轮子——更何况这只轮子已经在软件行业滚了几十年。

论文的出发点恰恰是:动态组合早已遍布现代软件,真正没有发展充分的,是它背后的形式化基础

所以,贡献并不在于“插件模式”本身,而在于把插件系统底下那些大家凭经验处理、却很少被严谨写清楚的规则,认真整理并证明出来。

两个经常被混为一谈的问题

任何由可插拔模块组成的系统,都绕不开两个难题。它们经常被打包成一个问题讨论,但实际上并不是一回事。

第一个问题与时间有关。

某个模块被移除后,它之前做过的事情怎么办?

它可能注册了事件处理器、打开了网络连接、修改了某些值、订阅了若干消息。几乎所有传统系统都把清理责任交给插件作者:房子退租时,请恢复原样,垃圾记得带走。

大多数开发者通常也会清理,至少主观上是想清理的。问题在于,遗漏往往安静得很:一个监听器没注销,一条连接没关闭,一小块状态没还原。单看每次都不严重,但积少成多,程序运行一下午后就开始莫名其妙地脚步虚浮,像连续开了八小时会却没吃午饭。

第二个问题与空间有关。

模块 A 依赖模块 B,但 B 可能还没出现,也可能运行到一半突然消失,甚至可能在 A 话说到一半时被换成另一个 B。

大多数系统只会在启动阶段连接一次依赖。接好之后,这些连接就被当成既成事实。倘若底层世界发生变化,轻则程序直接崩溃,重则继续抱着一个已经过期的对象工作——表面上风平浪静,实际上每一步都走错。

因此,“时空”并不是为了让论文标题显得高深。它对应的正是这两个维度,而论文的核心主张,是这两种保证能够同时成立

时间这一半:每次改变都随身携带撤销操作

这套机制靠的不是魔法,而是记账。这不是贬低,恰恰是称赞。

模块对系统做出的每一项改变,都必须经过框架。框架不仅记录发生了什么,还会记录对应的逆操作。按照论文的说法,每次变换都会携带一个由运行时追踪的逆变换。等模块被移除时,系统只需要倒着重放这些记录。

这很像把复式记账应用到了副作用上。

做复式记账时,你不会等到年底关账,才努力回忆:“三月份那笔钱到底花哪儿去了?”每一笔账发生时,对应的另一笔就已经同时登记,因此平账不再依赖某个人记性好不好。

这里也是同样的结构。清理不再是一项由开发者做得好或做得差的额外工作,而成为系统记录变化方式本身所具备的性质。

换句话说,不是提醒所有人“走的时候记得关灯”,而是让开灯这个动作天然附带一个可追踪的关灯操作。

空间这一半:不会睡死的依赖关系

另一半机制是:模块声明自己需要什么,然后由框架持续观察这些依赖。

依赖出现,模块启动;依赖消失,模块停止;依赖被替换,模块随之调整。

不需要反复轮询,不必因为依赖突然下线而崩溃,也不会继续对着一个早已离开现场的对象自说自话。

论文拿来对比的例子,Web 开发者应该很熟悉:React 的 useEffect。它允许你表达“请执行这段逻辑,并在适当时候这样清理”。但清理代码是否完整、是否正确,依旧是开发者自己的责任。忘记写很容易,写漏也很常见。

论文提出的不同之处在于:完整恢复不应只是开发者需要履行的一项义务,而应该成为系统自身能够保证的性质。

它没有承诺什么

到了这里,宣传文案其实应该比现在更谨慎一点。

这套保证只覆盖经过框架的操作

插件仍然可以直接写文件、修改运行时根本看不见的全局变量,或者启动一个新进程。如果这些行为没有进入框架的账本,移除插件时自然也就无法自动恢复。

因此,这项工作并没有让所有任意副作用突然变得可逆。它真正做到的,是让被记录的副作用可逆;然后进一步论证:如果所有变化都通过这套记录机制发生,就能得到很强的系统保证。

这依然是一个实实在在的成果,只是没有“一切皆插件”这类四词横幅听起来那么无边无际。值得肯定的是,论文主动划清了边界,并没有把这项工作留给挑剔的读者。

论文区分了两类行为:

  • 获取资源:例如打开文件、分配内存、启动进程。系统可以追踪这些行为,也可以执行相应的逆操作。
  • 通过资源向外发送内容:例如已经写入文件的字节、已经发出去的消息。数据一旦离开系统,就不是简单倒放录像能够收回来的。

到了第二种情况,框架只能依赖应用作者手动编写补偿逻辑,而且论文明确承认,它的元理论并不覆盖这部分。论文的表述是:如果某个位置无法被系统“具体化”,它就位于系统边界之外,自然也位于定理覆盖范围之外。

说得直白一点:框架可以帮你关掉水龙头,却不能保证已经流进下水道的水还能原路倒流回来。

那么,真正的成果是什么?

是证明。

论文从编程语言理论中取出两个概念:

  • 效应(effects):一段计算会对外部世界做什么。
  • 余效应(coeffects):一段计算需要从外部世界获得什么。

作者把它们从类型系统提升到运行时,再统一为一种“上下文”的概念。

接下来才是最难的部分:证明这种保证不仅对单个孤立组件成立,也能对整个组件系统成立——即使组件以任意顺序加入、离开,彼此操作交错执行,结论仍然不变。

真正的难点,就藏在“任意顺序”这四个字里。

让一个插件在退出时打扫干净,并没有特别困难。真正困难的是证明:无论组件以什么顺序加入和离开,无论重复多少次,最终系统状态都与“这些组件从未移动过”时完全一致。

这不是“我测试了几次,好像没问题”,而是要回答:“如果所有人同时进进出出,顺序还完全不可预测,这套机制为什么依旧不会乱?”

论文对前人的工作也相当坦诚。

它将 OSGi——也就是 Eclipse 插件架构底层使用的 Java 模块系统——称为最接近的先例,并认为自己的新增贡献主要是逆操作追踪与异步拆卸。

论文还讨论了 Erlang 的热代码重载。Erlang 可以在系统持续运行时替换代码,但状态迁移需要手工编写,而且它不会卸载组件,也不会回滚组件已经产生的效应。

至于 Spring、Guice 之类的依赖注入框架,依赖连接通常发生在初始化阶段,之后不会随着环境变化自动响应。

读过“相关工作”章节的人都知道,论文如此直接地承认哪些东西不是自己发明的,并不算常见。学术写作有时也像家庭聚餐:人人都愿意介绍自己带了什么菜,却不一定主动说这道菜以前谁做过。

它从哪里来

最后还有一件值得知道的事:这并不是实验室凭空造出一套理论,再寻找现实世界作为落脚点。

被形式化描述的运行时叫作 Cordis。早在这项研究成为新闻之前,它已经在开源聊天机器人框架 Koishi 中运行了多年。Koishi 长期主要由一位开发者构建和维护,而这位开发者也是论文的共同作者。

按照论文案例研究中的描述,这个生态已经经历“超过四年的开发”,并拥有“超过 4000 个由社区贡献的插件”。编写这些插件的人,大多并没有在脑中琢磨什么元理论,他们只是想把功能做出来,并让它正常运行。

所以,这个故事更准确的版本是:

有人先造出了一套确实能工作的东西,在开源环境中维护了很多年;后来,他和合作者坐下来,认真研究它为什么能够工作,以及其中哪些性质可以得到严格保证。

论文对于这段历史究竟能证明什么,也保持了应有的克制。

在有效性威胁部分,作者承认,现有证据“来自单一宿主语言中的单一生态系统”,无法将这套范式本身的优点与 TypeScript 实现的优点彻底分开,而且这些证据“来自观察,而不是受控比较”。

四千多个插件当然是个很不错的信号,但信号终究不是实验。一个夜市摊位连续排队四年,基本可以说明东西不难吃,却还不能直接写进营养学教科书。

最后还有一个重要提醒:论文目前将自己标记为仍在积极修订的预印本,而不是已经通过同行评审的研究成果。作者也明确表示,其中的内容未来可能发生较大变化。

因此,更合适的阅读方式是:把它看成一套正在完善中的严肃论证,而不是已经尘埃落定的最终结论。


免责声明:由人类撰写,并在适用之处使用 AI 改进。