第101期 | 一封帖子判 Linux 死刑，它怎么活下来的？

操作系统 · 2026-11-01 · 九羲科技

一、1992年，一封帖子判 Linux 死刑

1992年1月29日中午，阿姆斯特丹的 Andrew Tanenbaum 在 comp.os.minix 敲下一篇帖子，标题五个词，全大写：LINUX is obsolete¹。

判词三条：1991年还写宏内核，是"倒退回1970年代的一大步"；"真正设计操作系统的人中间，这场争论已经结束了，微内核赢了"；Linux 绑死 x86，而 x86 注定被取代。

Linus 当天深夜回帖²。回得硬：Minix 有先天缺陷（不支持多线程）；Linux 是他学 386 的练手之作，免费给出，不该被指责。回得也诚实：他亲口承认，微内核"从理论和美学的角度看"更优越——赢的人，当众说对方漂亮。

这场架吵出 73 帖，扯进 Peter MacDonald、David Miller、Theodore Ts'o 等后来的内核重臣。1999年，O'Reilly《Open Sources》把论战全文收进附录 A³，当"那个年代的人怎么想操作系统"的标本。

孙过庭《书谱》有句："贵能古不乖时，今不同弊"⁴——作书最忌泥古与趋时。Tanenbaum 判 Linux 泥古，Linus 判微内核趋时：理论漂亮，跑起来未必。三十四年后再看，两句判词各对一半：x86 没死；微内核也没死，活在别处。

二、AI 先选边

信任比结构更贵：如果 AI 的操作系统先出现，它会选宏内核，还是微内核？

上周，2026年10月30日，seL4 17.0.0 发布⁵——全世界唯一形式化验证过的微内核：2009年机器检验的代码级证明完成，2014年代码与证明全部开源。发布说明很老实：这次修的，是"形式化证明覆盖不到的配置"里的问题。而报出这些问题的，是 Anthropic：一家 AI 公司，用 AI 做的安全审计，把"被数学证明过"的内核又审了一遍。

1987年，Brooks 在《No Silver Bullet》里审讯"程序验证"这个候选银弹，判词是：证明只能证明程序符合规格，而最难的，恰恰是把规格本身调试对⁶。三十九年后，seL4 的发布说明亲口应验：证明管的是范围内的事，范围之外，仍是荒野。微内核赢了纯粹性，但纯粹性本身有边界——Brooks 说的"本质困难"那一侧，验证手段够不着。

1992年争的是结构，2026年争的是信任。Linus 赢了结构之争：生态、驱动、三十年工程复利。Tanenbaum 的阵营在信任之争里还活着：seL4、Fuchsia 的 Zircon、每颗 Intel CPU 管理引擎里跑着的 Minix 3。AI agent 时代，"不可信代码"是常态：智能体天天跑第三方工具、调第三方模型，"谁可以碰谁"比"跑得快"更重要。微内核等了三十四年，等来的不是平反，是一道新题。

三、今晚，数一数你内核里的驱动

找一台手边的 Linux 机器，三个动作。

数驱动：ls /lib/modules/$(uname -r)/kernel | wc -l——"内核一半代码是驱动"，不是比喻，是行数。

看代价：seL4 微内核约一万行 C，Linux 内核约三千万行（据公开资料）。多出来的两千九百九十九万行，买的是什么？装一份源码跑 sloccount，自己数一遍。

读原帖：linfo.org/obsolete.html，1992年1月29日一天之内的一来一回。注意 Linus 的语气：他没说微内核错了，他说的是"我现在就要一个能跑的东西"。

"结构—代价—取舍"三段式，做 AI 工程可以直接抄：边缘 AI 盒子选 OS 底座，选题清单就是这场论战留下的——要生态和驱动，宏内核；要隔离和可验证，微内核。没有银弹，先过 Brooks 的 9/10 检验⁶，再谈情怀。

宏内核 vs 微内核：左边把调度、内存、文件系统、驱动全装进内核态一个大方块；右边只留调度、IPC、内存原语在内核，服务全搬进用户态，用消息传递说话。1992 年吵的，就是这张图。

· · ·