Wonderland — 2026-11-01

Wonderland — 2026-11-01

速览（30 秒）
  • 组合: 编译器与编程语言设计 × 形式化方法与定理证明 / 免疫学与疫苗学 × 博弈论与机制设计 / 音乐理论与声音设计 × 钟表学与精密计时史
  • 今日火花 Top 3: #1 把证明扔掉，只留一个能重放的小检查器 / #5 沙宾不要专利：把价格设成 0 的机制 / #8 PC 的串口芯片也怕全零：8251A 那个”对方停机了”的位
  • 可动手候选: #4（用一张 1.44M 软盘跑一次 TCC 自举）、#6（给自家项目算一遍”搭便车”收益）、#9（写 20 行 HDB3 编码器标出违规位）
  • 值得写长文: #2（编译器与证明器共用一个母语）、#7（没有设计者的市场）、#10（平行五度与全零串是同一条禁令）

组合 A：编译器与编程语言设计 × 形式化方法与定理证明 + 如果只能使用 1KB 内存

本期亮点: 1KB 这条约束没有让这条路变窄，反而把它逼成了一条分工线：线内的东西要能逐行读完，线外的东西只能相信。这一组的三张卡分别落在”检查器""母语""种子”上——都是当代编译与证明工程里真实存在的、巴掌大的小东西。

💥 #1 — 把整个证明扔掉，只留一个能重放的小检查器

方法论惊讶 9 · 具体 9 · 可行 7

Lean4Lean 用 Lean 自己写出了另一个完整的 Lean 4 类型检查器，证明除了官方那个 C++ 参考实现之外，第二个检查器同样能核验 Lean’s mathlib；另一条更省的路子是 Coq 的 coqchk——一个脱离证明环境、只吃编译好的 .vo 的独立检查器，命令行里还专门留了个 -m 选项报告”检查器自己吃了多少内存”。在 1KB 的机器上，可信的唯一办法不是更聪明的检查器，而是把中间产物全部扔掉、只留下能被小检查器重放的东西。

如果要做装一个 Coq，跑 `coqchk -m` 看看检查整个标准库到底吃多少内存；然后把所有证明对象删掉、只留 .v 脚本重新编译一遍，比较两边各自的可信成本。

参考文献 1
  1. arXiv:2403.14064（Lean4Lean: Verifying a Typechecker for Lean, in Lean）/ arXiv:2607.12226（FLEX：把可信基”reduces the trusted base to the kernel alone”）/ 旁证：coqchk 手册页（“the standalone checker of compiled libraries (.vo files produced by coqc)“，含 -m —memory 选项）
生图提示词

一间巨大的档案室里，成山的证明卷宗被推入焚化炉，只剩一条细细的脚本带子滑进一台火柴盒大小的机器，机器吐出一枚绿色对勾。

img-2026-11-01-1.png

💥 #2 — 编译器与证明器共用一个母语：ML 原本是给定理证明写的

同构惊讶 8 · 具体 9 · 可行 6

ML 的全名就叫 Meta Language——它 1973 年在爱丁堡被造出来，唯一的用途是给 LCF 定理证明器写证明战术；而 Hindley–Milner 类型推断（今天 OCaml、Haskell、Scala、Elm 这一大家族的类型系统内核）第一次就是实现在 ML 里的。现代编译器用来判断”这段程序能不能活”的那套算法，是从定理证明器的战术语言里长出来的。

如果要做用 200 行写一个迷你 Algorithm W（并查集 + 约束生成），只处理多态与函数类型；跑通之后你会发现，你在纸上写的其实是当年那批证明战术的简化版。

参考文献 1
  1. Wikipedia “ML (programming language)”（“ML (Meta Language) is the metalanguage developed for the Edinburgh LCF theorem prover in the 1970s”，1973 年由 Robin Milner 与学生助手在爱丁堡开始）/ Wikipedia “Hindley–Milner type system”（“It was first implemented as part of the type system of the programming language ML”）
生图提示词

一棵大树的根系扎在刻着 LCF 的石座上，树干上刻着 ML，枝桠分别伸向 OCaml、Haskell、Scala 三块木牌。

💥 #3 — 可信基是一条线，不是一个体积：线这边逐行读，线那边只能信

文化隐喻惊讶 8 · 具体 9 · 可行 6

HOL 家族整个架构只赌一件事：定理是一个抽象数据类型，只有内核里那几条推理规则能造出新的定理，于是”a large system can be built on top of a small trusted kernel”；Andromeda 把这个赌注推到极致——唯一可信的部分是一个极简核，连相等性判断都下放给用户自己写的代码。1KB 不是压缩指标，是分界线：线内可以逐行审计，线外只能选择相信。

如果要做把你项目里”绝对不能错”的那段代码单独拎出来（解析、鉴权、密钥处理），数一数它有多少行；再数一数其中有多少行是别人写的、而你从没读过。

参考文献 1
  1. Wikipedia “HOL (proof assistant)”（“As such, a large system can be built on top of a small trusted kernel”）/ Wikipedia “Logic for Computable Functions”（定理是抽象数据类型，只有对应的推理规则函数能造出新定理）/ arXiv:1802.06217（Andromeda：唯一可信组件是 minimalist nucleus，等值检查下放给用户）
生图提示词

一条细如发丝的亮线横过一张巨大的图纸，线的这一侧堆满密密麻麻的手写符号，另一侧只有一枚黄铜印章和一小叠纸。

💥 #4 — 自举的种子必须先被相信：TCC 是一张 1.44M 软盘上的编译器

装置/原型惊讶 8 · 具体 9 · 可行 8

Tiny C Compiler 的 x86 可执行文件约 100 KB，能直接从一张 1.44M 软盘上启动运行；Bellard 的官方基准里 TinyCC 0.9.22 编译速度约 85.9 万行/秒，GCC 3.2 -O0 约 9.8 万行/秒。在 1KB 的世界里，编译器第一个要回答的问题不是”能不能编译”，而是”你敢不敢先运行一个别人写的二进制”。

如果要做把 TCC 编译一遍它自己的源码（自举），再用两个产物互相编译第三轮，比对输出是否逐字节相同——你会亲手得到一句”我可以相信它”。

参考文献 3
  1. Wikipedia “Tiny C Compiler”（“about 100 KB for the x86 TCC executable”，可直接从单张 1.44M 软盘启动运行）/ bellard.org/tcc 官方基准表（TinyCC 0.9.22：2.27s
  2. 859000 lines/s；GCC 3.2 -O0：20.0s
  3. 98000 lines/s）/ 旁证：Wikipedia “Tiny C Compiler” 的自举实验记录（用 TCC 编译 GCC 的 cc1：用时 1145 秒，而由 GCC 3.4.2 编译的 cc1 需 518 秒）
生图提示词

一张微微翘起的 1.44M 软盘躺在桌面上被塞进老式机箱，机箱吐出一枚指甲盖大小的芯片，芯片上浮着一圈极细的光环。

组合 B：免疫学与疫苗学 × 博弈论与机制设计 + 如果预算只有 0 元，只能用 GPL/BSD/MIT 开源组件

本期亮点: “0 元预算”这条约束把问题推到了最硬的地方：没有钱可以买规则，只能靠规则本身让所有人都愿意参与。这一组的三张卡讲的是同一件事的三个面——免疫系统是一个公地、一张免费的许可证、还有一个完全没有设计者的市场。

💥 #5 — 沙宾不要专利：把价格设成 0，是覆盖率最高的机制设计

文化隐喻惊讶 9 · 具体 9 · 可行 7

沙宾拒绝为口服脊灰疫苗申请专利，并在 1972 年把生产所需的病毒毒株无偿捐给世界卫生组织；2021 年牛津/阿斯利康把新冠疫苗定成”疫情期间非营利、对中低收入国家永久非营利”的价格，到十亿剂时依然免费分发。当预算为 0，最大的协调工具不是补贴也不是定价，而是把价格本身设成 0——开源 copyleft 用的正是同一招：你可以免费用，但你必须把衍生品也放出来。

如果要做给你自己的项目写一份”0 元版”授权条款：允许任何人免费使用、禁止闭源衍生、要求改动也公开——看看三个月后有多少人真的来了。

参考文献 1
  1. 维基百科中文版「阿尔伯特·沙宾」与「脊髓灰质炎疫苗」（沙宾拒绝为脊灰疫苗申请专利，1972 年将其疫苗生产所用的病毒毒株无偿捐赠给世界卫生组织）/ 牛津大学新闻稿《One billion doses of Oxford-AstraZeneca COVID-19 vaccine released》（2021-07-29：“on a not-for-profit basis for the world during the pandemic, and in perpetuity for low- and middle-income countries”）/ 旁证：Wikipedia “Copyleft”（copyleft 是”在要求衍生作品保留同样权利的前提下授予复制品某些自由”的法律技术）
生图提示词

一只手里举着的专利证书被折成纸飞机推上天空，纸飞机飞向一顶敞开的白色帐篷，帐篷外排着看不到头的人队，每个人手里都攥着一张免费接种卡。

img-2026-11-01-2.png

💥 #6 — 群体免疫是免疫学里的公地：免费搭车是它的稳态

方法论惊讶 8 · 具体 9 · 可行 7

最新的流行病学博弈综述把群体免疫直接写成”阈值公共品博弈”：免疫者是合作者，易感者是搭便车者；一旦群体免疫比例越过阈值，继续接种的个体收益就低于不接种。“保护所有人”这件事在个体层面是搭便车、在群体层面却是唯一的解——一台没有预算的机器只能靠规则运转，而这条规则一旦跌破阈值就会自己垮掉。

如果要做拿一个你参与的社区（公司、开源项目、小区）当样本：算一遍”大家都守规则”与”总有人搭便车”两种情况下你的收益差多少，再决定要不要主动去当那个补缺口的人。

参考文献 1
  1. 10.1007/s13235-025-00619-5（Public Goods Games in Disease Evolution and Spread, Dynamic Games and Applications 15:1733-1749, 2025：herd immunity 作为阈值公共品，免疫者=合作者、易感者=搭便车者）/ 10.1109/tcss.2019.2896227（Modeling Behavioral Response to Vaccination Using Public Goods Game, IEEE TCSS 6:268-276, 2019）
生图提示词

一圈人围成方阵站在发光的免疫围墙内，围墙缺了一个口子，缺口附近的人一个接一个往后退，退出来的空隙让缺口越撕越大。

💥 #7 — 免疫系统是世界上唯一没有设计师的市场：多样性靠随机，筛选靠机制

同构惊讶 8 · 具体 9 · 可行 6

抗体的多样性不是被设计出来的，而是 V(D)J 重排随机生成出来的——1974 年的 PNAS 与 1983 年 Nature 两篇论文给出了体细胞重排的直接证据——克隆选择学说负责事后筛选。这是一台”先随机生产、再由环境选择”的市场，等价于演化博弈里的选择压力，而不是机制设计里的规则设计：自然界里唯一一个运行着机制设计、却没有设计者的市场。

如果要做做一个 20 行的模拟：随机生成一百万把”钥匙”（随机形状），只用一把去试锁（环境筛选），统计命中率的分布——你会看到随机的广度远胜精心设计的全集。

参考文献 1
  1. 10.1038/302575a0（Somatic generation of antibody diversity, Nature 302:575-581, 1983）/ 10.1073/pnas.71.10.4027（Evidence for Somatic Generation of Antibody Diversity, PNAS 71:4027-4031, 1974）/ 旁证：10.1007/s10238-009-0048-y（Burnet and the clonal selection theory of antibody formation, Clinical and Experimental Medicine 9:253-258, 2009）
生图提示词

一台巨大的自动售货机哗啦啦滚出成千上万把形状各异的钥匙，钥匙落进传送带尽头的一把锁，只有一把卡住并亮了起来。

组合 C：音乐理论与声音设计 × 钟表学与精密计时史 + 如果必须兼容 DOS/8086 时代的中断处理

本期亮点: 这一组接着上一期那张卡往下追了一层：接收端到底怎么知道自己站在哪儿？答案是——协议一代比一代更省地使用”标记”，从显式的帧同步位，到故意违规，到被保留的符号；而乐谱与擒纵机构早就在用同一套办法定义语法。

💥 #8 — PC 的串口芯片也怕全零：8251A 有一个”对方停机了”的位

装置/原型惊讶 8 · 具体 9 · 可行 8

8086 时代的 8251A USART 上有个 SYNDET（break detect）位：接收端连续两个字符时序都是低电平（也就是收到一串全零）它就置位报警；而在电话线上，贝尔系统的 T1 载波恰恰是为了保证线上永远不会出现全零字，才必须在每帧 193 位里塞一个同步位。同一件事在两个年代、两种器件上各写了一遍：一台机器靠”检测到全零”报告失联，另一台机器靠”绝不允许全零”维持不失联。

如果要做用 Arduino 的 UART 故意发一段 0x00 连击，打开接收端的 break 检测，看它多久报一次错；再把这段全零塞进一段正常数据中间，看看接收端怎么把”帧”搞乱。

参考文献 2
  1. Intel 8251A 数据手册（BREAK DETECT（仅异步模式）：“This output will go high whenever the receiver remains low through two consecutive stop bit sequences (including the start bits, data bits, and parity bits)“；FE
  2. Framing Error：“A valid stop bit is not detected at the end of every character”）/ Wikipedia “Intel 8251”（8251A 商用版 1980 年 5/6 月发布，定价 $6.40，被 Intel SDK-86 MCS-86 系统设计套件采用）
生图提示词

一块绿色老电路板上的 28 脚芯片，脚边一排小灯；画面中央一根长铜缆上滚过一片发光的白色方块，滚到芯片前时芯片上的一盏红灯突然亮起。

img-2026-11-01-3.png

💥 #9 — 每一代协议都在删掉那个”标记位”：最后只剩一个必须出现的违规

方法论惊讶 8 · 具体 9 · 可行 7

SONET 的一帧是 9 行 90 列共 810 字节，最前面 3 列是传输开销，A1、A2 两个字节就摆在帧首——那是最笨也最稳的显式标记；E1 线路的 HDB3 改用”故意插入双极性违规”来阻止长串零让接收端失步，违规码（000−、000+、+00+、−00−）该选哪一个，取决于”距上一个违规位 V 以来正负脉冲的计数是奇是偶”；到了 10G 以太网，64b/66b 干脆规定 ‘00’ 与 ‘11’ 两种块类型”故意不用”，只让接收端去找 ‘01’/‘10’ 的跳变。标记位从一个专门的字节缩成一个模式，接收端要靠数违规位之间的历史来恢复位置——这是一台把状态藏进计数里的机器。

如果要做用 Python 写 20 行 HDB3 编码器，喂它一段含长串零的数据，把编码结果和违规位标出来；再写一个只靠跳变恢复时钟的解码器，看它在没有违规位时会失步多久。

参考文献 2
  1. Wikipedia “Modified AMI codes”（HDB3
  2. B8ZS：“deliberate bipolar violations are inserted into the line code, to create a sufficient number of transitions to maintain synchronization”；违规码 000−/000+/+00+/−00− 的选择规则）/ Wikipedia “64b/66b encoding”（“provide enough state changes to allow reasonable clock recovery and alignment of the data stream at the receiver”；协议开销 3.125%，此前 8b/10b 为 25%）/ 旁证：Wikipedia “PCI Express”（PCIe 1.x 用 8b/10b，原始信道开销 20%，2.5 GT/s 的标称其实是编码后的速率）/ Google Patents US6493359B1（SONET STS-1 帧 = 90 列 × 9 行 = 810 字节，前 3 列为传输开销，A1/A2 位于帧首）/ 8b/10b 的 K28.5（Comma）：接收端字对齐电路靠检测这个特殊符号确定 10 位符号的边界，PCIe 用 K28.1/K28.7 表示链路训练状态
生图提示词

一条深色线缆上滚动着黑白相间的方块，其中偶尔有一个被涂成刺眼的红色（违规位），缆的尽头一只小眼睛正数着红色方块之间夹了多少个白块。

💥 #10 — 平行五度与全零串是同一条禁令：语法靠”不允许发生的事”来定义

同构惊讶 7 · 具体 9 · 可行 7

严格对位法禁止平行五度与平行八度，理由不是它们单独难听，而是”它们制造出彼此的移位副本、抹掉两个声部的独立性”（八度移位也不影响判定）；而在机械钟里，1715 年乔治·格雷厄姆的”死擒纵”把擒纵轮的静止面做成与叉轴同心，让轮子”永不回退（never recoils）“。禁止一种运动，比事后修正一种运动便宜得多：乐谱、线路、擒纵机构，三样东西都是用禁令而不是纠正来定义自己。

如果要做找一张古典对位谱，用软件标出所有平行五度；同时把一段 HDB3 编码流里的违规位也标出来——两张图并排放，你会发现”标记”和”禁令”是同一种图。

参考文献 1
  1. Wikipedia “Consecutive fifths”（“create parallel melodic lines, melodies that are duplicates of each other, transposed”；“Octave displacement is irrelevant to this aspect of musical grammar”）/ horopedia “Graham escapement”（1715 年的 dead-beat pallets，静止面与叉轴同心，轮子永不回退）/ 旁证：Wikipedia “Escapement”（锚式擒纵的”recoil”会扰乱摆动、造成走时不准；死擒纵因精度更高在 19 世纪取代了锚式）/ 10.2307/854227（Voice Leading in Post-Tonal Music, Music Analysis 9:177, 1990）
生图提示词

一张摊开的乐谱上，两道平行的金色声部轨迹被一根红叉划掉；轨迹旁边是一只拆开的钟表擒纵机构，擒纵轮的齿在红色的禁止扇区前停住。