{"id":"mb-20260828-7fb065","account":"mubei","brand":"","title":"一个 AI 用了一周时间，把整个底层压缩库 zlib 彻底重写了一遍","summary":"一个 AI 用了一周时间，把整个底层压缩库 zlib 彻底重写了一遍","body":"一个 AI 用了一周时间，把整个底层压缩库 zlib 彻底重写了一遍。\n它没有提交任何单元测试。\n它交出来的是整整 32,000 行纯数学证明。\n一个只有几千行代码的独立微内核，把每一行逻辑从头到尾验算了一遍。\n全部通过。\n很多人聊起 AI 编程，焦点全在模型写代码有多快、能写多少行。\n真正的致命危机发生在另一头。\n当自动化编程代理每周向代码库倾倒成千上万个合并请求时，软件工业现有的所有质检手段，全部失效了。\n让大模型给代码打分，本质是概率猜概率，两层幻觉相互掩盖。\n单元测试只能覆盖工程师预先想到的边界，测不到没想到的死角。\n人工代码评审的精力，在机器每秒几千行的吞吐量面前，连零头都接不住。\n三套传统防线加在一起，没有一套能向你保证：这段代码在面对所有可能输入时，绝对没有漏洞。\n如果连写代码的人都无法验证结果，成倍暴涨的 AI 生产力，到底是在创造资产，还是在疯狂堆积灾难？\n要解开这个死结，必须把软件工程沿用了半个世纪的分工彻底掀翻。\n这台机器叫：形式化验证与规约所有权。\n它的核心载体，是正在硅谷重构代码底座的交互式定理证明语言 Lean 4。\n过去写软件，人类既要费劲写业务实现，又要写一堆测试用例去碰运气。\n在这套新体系里，人类退守到了唯一不可替代的位置：定义形式化规约。\n人类只用严格的数学逻辑写下系统的铁律：解压后的输出，必须与压缩前的输入完全恒等。\n怎么写出实现代码，怎么证明代码在所有情况下都满足这条铁律，全部交由机器解决。\nAI 在背后的推导过程，就像在一张无限大的棋盘上下棋。\n它把庞大的最终定理拆解成成百上千个微小的引理。\n每推进一步证明策略，就尝试闭合一个逻辑分支。\n一旦推导陷入死胡同，立刻自动回溯换路，直到所有分支全部被推导至终局。\nAI 生成的这三万多行证明代码，被送进一个精简的独立验证内核。\n这个内核完全开源，代码量极小，不包含任何大模型黑箱。\n它只做一件事：用确定性的类型论规则，做纯粹的符号验算。\n只要内核判定通过，这段代码在数学意义上就是绝对正确的。\n不是在一百万次抽检里碰巧没报错。\n是在无穷无尽的输入空间里，从数学逻辑上断绝了一切出错的可能。\n这套机制早已走出了学术论文，变成了支撑顶级云厂商运转的工业流水线。\nAWS 的开源权限系统 Cedar，已经在生产环境里全天候运行这套逻辑。\nCedar 的核心授权语义全部用 Lean 4 编写规约并完成数学证明。\n真正上线跑业务的高性能代码，则用 Rust 编写。\n每天晚上，AWS 的自动化测试集群会在两者之间狂跑 1 亿次差分测试。\n只要 Rust 生产代码的运行结果和 Lean 4 的数学规约出现一丝一毫的偏差，版本立刻被拦截，一行代码都不准发布。\n过去几十年，程序员把绝大部分生命耗费在把人类语言翻译成机器指令上。\n验收依赖于有限的抽样用例，以及注定会疲劳的人肉眼球。\n当 AI 让写代码的边际成本归零，代码本身就降级成了廉价的推论副产品。\n真正决定系统生死和商业价值的，只剩下了人类写下的那一纸数学规约。\n未来的软件构建，不再是人教机器怎么写逻辑，再祈祷测试跑通。\n是人类锁定数学真理的边界，机器在里面完成穷尽证明。\n当代码能够被数学证明的那一刻，软件才真正从一门碰运气的经验手艺，变成了精密可靠的现代工程。","category":"科技","score":null,"translated_x_url":null,"translated_status_id":null,"published_at":"2026-08-28 21:55:48","created_at":"2026-08-28 21:55:48"}