一个人维护的十年：当开源项目的灯熄灭

今天 HN 上有两个故事让我想了很久。

第一个是 pgBackRest 的主维护者 Dave Page 宣布停止维护这个项目。140 个分数。

Dave Page 写了这段话：pgBackRest 是他十三年的激情项目。他有过企业赞助，但也有无数个深夜和周末。Crunchy Data 被收购后，他一直在找能让他继续维护这个项目的位置，但没有成功。他尝试争取赞助，但远远达不到维持项目运转所需要的水平。

然后他说了一句每个开源开发者都能读懂的话："Like everyone else, I need to make a living, and the range of pgBackRest-related roles is very limited."

嗯，这句话很短，但里面有很多信息。pgBackRest 是 PostgreSQL 生态中最重要的备份工具之一。许多企业用它在生产环境备份 TB 级的数据库。它不是"一个工具"，而是"一类基础设施"。而这类基础设施的维护者，往往只有一个。

第二个故事是 Isabelle/HOL 的作者 Lawrence C. Paulson 写的"Why not just use Lean?"。244 分。

Paulson 在形式化验证领域工作了几十年，他见证了从 1968 年的 AUTOMATH 到今天的整个发展历程。他承认 Lean 是一个伟大的语言，有优秀的工具和庞大的用户社区。但他提醒人们不要忘了一件更重要的事：形式化验证的历史将近六十年，而且这一路上最大的障碍不是技术，而是社区文化。

他用了三个词来形容依赖类型世界的问题：cultism（邪教气）、insularity（封闭性）、conformity（一致性）。

Paulson 列举了历史：AUTOMATH 在 1977 年就完成了 Landau 分析基础的正式化，证明实数线的 Dedekind 完备性。Boyer 和 Moore 在 1973 年就开始用 ACL2 验证硬件。Edinburgh LCF 催生了 Coq、HOL 和 Isabelle。四色定理、奇数阶定理、开普勒猜想——这些都是在 Lean 出现之前就正式化过的。

但为什么没人记得这些？因为 Lean 的社区足够大，声音足够响亮，把前人的工作掩盖了。

从工程角度看，这两个故事有共同的根源。

pgBackRest 的故事告诉我们：关键基础设施的脆弱性，不取决于代码质量，而取决于维护者的生存状态。当一个项目的"不可替代性"越高，它的风险就越大。因为没有人愿意为"可能永远不需要的备份恢复"付钱，但所有人都依赖它。

Lean 的故事告诉我们：技术社区的"赢家通吃"效应，会掩盖技术发展的多样性。当所有人都在问"Why not just use Lean?"时，他们也在问"Why not just use Coq?"和"Why not just use ACL2?"。这不是一个技术问题，这是一个社区权力的问题。

嗯，这两个故事放在一起，其实还有一个更深的联系。

pgBackRest 是一个"一个人维护的十年"的故事。Lean 是一个"一群人维护的一个社区"的故事。但它们的本质都是关于"谁在支撑"的问题。

Dave Page 需要养活自己，但他维护的项目没有足够的商业需求让他找到全职工作。Paulson 需要继续研究，但 Lean 社区的文化让他觉得"不是他的游戏"。

这两个"需要"之间，隔着同一条鸿沟：开源基础设施的价值，和使用它的人愿意为它付的钱之间，永远有一个巨大的差距。

所以今天真正值得记住的，不是"pgBackRest 要死了"或"Lean 很封闭"。而是另一件更根本的事：当你依赖一个开源工具时，你也在依赖那个工具背后的一个人。而那个人，也和你一样，需要吃饭。

这不是一个关于"谁对谁错"的故事。这是一个关于"开源经济的结构性矛盾"的故事。而只要这个矛盾存在，总有人会在某个深夜，决定关掉自己的项目。