Back to Home
AI2026年8月15日5分钟阅读

DeepSeek Harness底层的Cordis使用了一种面向时空可组合性的编程范式

有了AI,我的文化水平又可以了

DeepSeek Harness底层的Cordis使用了一种面向时空可组合性的编程范式

DeepSeek Harness 终于发布了

随着年初 OpenClaw 的火爆,agent 大战已经持续半年多了。目前公认最好的 agent 产品应该是 Codex 和 Claude Code 吧。不过在大众场景下,国产 agent 工具也已经迎头赶上,豆包、WorkBuddy,应该是很多人的首选。

不过这些工具似乎都大同小异,更多的还是要依靠模型本身的能力。而 DeepSeek Harness 的出现或许可以开启一段不一样的发展趋势,因为它跟其他家的 agent 工具都不一样,极其灵活的插件模式让这个产品可以有无限的想象空间。

我觉得平时高强度使用 agent 工具的小伙伴们都应该来尝试一下,不是说它现在有多强,毕竟还是个开发者预览版,而是看看你还没能解决的一些问题,是不是在 DeepsSeek Harness 上可以找到解决方案。

我不前两天还在为几十个不太好管理的 Skills 苦恼吗,也许未来就要改成为 Harness 插件苦恼了。Harness 非常的插件化,就连核心功能都是靠一个个插件完成的。而实现插件化管理的核心,是它底层依赖的一个框架 Cordis。

Cordis

我对这样的框架很感兴趣,自然要去探察一番。Cordis 最初是为聊天机器人框架 Koishi 而设计的,这两个框架的作者都是 Yifan Shi,一个响指打得还不错的小伙,也是 DeepSeek 的成员,他应该是参与过 V3 系列模型开发的。

随着 DeepsSeek Harness 的发布,还有一篇 Cordis 的论文也跟着发表了,Yifan Shi 就是论文的一作。可能是我文化水平不够,还是头一次看到用数学公式来证明软件架构的。好在如今有了 AI,在 AI 的帮助下把论文看完了,我觉得自己的文化水平又可以了。

A Programming Paradigm for Spatiotemporal Composability

你看这论文标题,面向时空可组合性的编程范式,还挺有科幻感。不过它讨论的问题并不复杂,就是一个可热插拔的插件框架。

我们把这个挺有科幻感的概念「时空」解释清楚了,你也就明白了。它们一个是时间维可组合性(Temporal Composability),一个是空间维可组合性(Spatial Composability)。

时间维可组合性

时间维可组合性关注的是,当你删除一个组件时,必须能完全撤销掉添加它时,对系统环境的影响。

具体说就是当我们向系统添加组件时,必然需要定义这个组件对系统环境做了什么操作,那同时,我们也应该定义一个逆向操作,并记录在系统中,这样当我们从系统中删除这个组件时,就可以通过这个逆向操作来消除添加时产生的变化了。

理想的状况就是当我们卸载了一个组件后,系统环境的状态应该和安装它之前是一样。而且多个组件之间,在没有依赖关系的情况下,安装与卸载都是不依赖顺序的。例如你安装了甲乙丙三个组件,不论以什么顺序卸载,只要卸载了三个组件,那么系统环境就应该和安装之前是一样的。

空间维可组合性

空间维可组合性关注的是组件间的依赖关系,要结构化的,声明式,说白了就是要维护一套依赖的拓扑结构。

目的是,当向系统添加或删除组件时,有依赖关系的组件可以及时做出响应。比如,组件甲依赖组件乙,当我安装组件甲时,应该首先检查是否存在组件乙,如果不存在,虽然安装了组件甲,但它应该保持未激活状态,无法使用,而不是使用的时候会报错。

而当我安装组件乙时,组件甲应该能够及时知道自己的依赖项已经就绪了,于是自己应该被激活。卸载也是,如果我要卸载组件乙,那么应该先让组件甲变为未激活状态,然后再卸载组件乙。这些过程都应该是框架自动完成的,不需要组件自己处理。

形式化证明

说是有88页论文,但其实最核心的内容就是这么点儿事,其它的就是一些实现细节和证明过程了。例如,多个有依赖关系的组件进行安装卸载时,每一个执行动作都是如何编排的,它们的生命周期是什么等等。

其实对于我们开发人员,这些热插拔的逻辑并不新鲜,很多人都做过,我也做过。说句自大的话,你让我写这么个热插拔框架我也能写出来,但是,如果没有这么一篇论文打底,我不可能比他们写得更好。

我很喜欢论文里的形式化证明,可能算是我的舒适区吧,只可惜咱这文化水平差些,很多基础知识当年都没学过,所以也看不懂。咱就说下面这公式:

Γ→Γ×(Γ→Γ)Γ → Γ × (Γ → Γ)

你没学过的能看懂这是啥,可是如果把它写成代码:

type RevertibleEffect = (
    before: Context 
) => [
    after: Context, 
    rollback: (current: Context) => Context 
]

大部分程序员应该都能看懂。我也问了下 AI,它这套方法属于形式化方法(formal methods)这个大类下的编程语言元理论(PL metatheory)分支。

计算机专业本科应该是会学一些这方面课程的,无奈咱是兴趣打底,半路出家,就没听过这专业课。可是我又一想,就算我当年学了,就肯定能听懂吗,其实也未必,也就不那么纠结了。

我之所以现在对它感兴趣,是因为我已经有很多开发经验了,然后看了这篇论文就会发现它其实是能解决很多问题的。这篇论文之于框架就是一种架构设计,我自己做架构设计也要去想这些问题,只不过是用普通的语言和逻辑去设计。而这种形式化证明的方法是不是会更严谨,更有效呢?

有 AI 真好啊,什么东西有了兴趣都可以跟着 AI 学,就是脑子可能有些迟钝了,慢慢来吧,硬件如此也没法着急。

感兴趣的小伙伴们也来读读这篇论文吧,可以让 AI 帮你解读,懂一些编程的话应该还是不难看懂的。

https://github.com/cordiverse/paper

行啦,我去做点 Harness 的插件吧。