从 Cookie 信号到 Lean 证明，软件正在把规则写进机器 (2026)

先看结论

这次 Hacker News 热榜里最有意思的变化，不是又多了几个 AI 产品，而是几种原本藏在经验、设置或口头约定里的规则，开始被写成机器可以读取和执行的接口：浏览器用信号表达隐私偏好，Cloudflare 按用途区分 AI 爬虫，Debian 讨论怎样记录和约束 LLM 辅助贡献，Ruff 把更多检查规则变成默认行为，Lean 则把压缩算法里的不变量交给证明器核验。

它们处理的对象完全不同，冲突却很像。规则如果只有一个模糊的「大家都知道」，就很难执行、迁移和追责；规则写得越具体，机器越能帮忙，但误判、升级和退出成本也会被摆到明面上。

下表的分数和评论数是抓取 Hacker News 当前 news / front 页面时的快照，不是永久排名。前四条出现在 7 月 26 日的 front 日榜，Lean 帖子出现在当前 news 页；它们也不是同一天发布的新闻。

五条热门帖，五种规则接口

帖子	抓取时热度	它把什么写成了规则
Kill The Cookie Banner	771 分，377 条评论	把隐私意愿从一次次弹窗改成浏览器与网站之间可复用的信号。1
Cloudflare's new AI traffic options for customers	187 分，143 条评论	把 AI 爬虫拆成 Search、Agent、Training 三种用途，再按用途配置放行和阻断。2
LLM Usage in Debian: Three Proposals	206 分，204 条评论	把「能不能用 LLM」改写成贡献来源、披露、责任和敏感信息处理规则。3
Ruff v0.16.0	332 分，221 条评论	把原先需要手动打开的检查项，变成升级后默认会运行的代码质量门槛。4
We have proof automation now	37 分，3 条评论	把压缩算法的隐含前提写成 Lean 可以检查的定理，让自动化产物不止是代码。5

五个 HN 提交者的个人背景在本轮可读材料中都没有得到独立核实。以下把原文作者、项目身份和社区讨论分开写，不把提交者误当成原文作者。

「Kill The Cookie Banner」是欧洲多个民间组织共同发起的倡议。页面主张把隐私偏好预先写进浏览器，由设备向网站或应用自动传递接受、拒绝或限制追踪的选择。倡议页面还称，欧盟委员会在 2025 年秋季提出过类似的自动信号方案，并把它放进更大的 Digital Omnibus 改革中；页面同时声明，它不支持改革中的其它部分。6

这个方案针对的不是 cookie 这个文件格式，而是网站把必要会话、广告追踪和跨站识别塞进同一个同意流程。HN 评论里有人指出，登录所需的 session cookie 不等于同意追踪；也有人提醒，禁用 cookie 可能影响验证码、防火墙和依赖会话状态的站点。评论区提出的折中方案是：默认限制非白名单站点，但给确实需要登录的站点保留必要会话。1

浏览器信号解决了重复点击和诱导界面，却仍要回答两个问题：网站是否必须遵守信号，必要状态能否与商业追踪分开。Do Not Track 已经说明，没有法律或平台执行力的信号，很容易退化成礼貌请求。

2. Cloudflare：AI 爬虫开始被要求说明自己要做什么

Cloudflare 在 2026 年 7 月 1 日发布的文章里，把自动化流量分成 Search、Agent 和 Training。Search 是收集或索引内容，准备之后响应查询；Agent 是代表用户实时完成任务；Training 则是把内容用于训练或微调模型。按这三类用途管理流量的选项向所有 Cloudflare 客户开放，包括免费套餐。7

Cloudflare 还宣布，2026 年 9 月 15 日起，新接入域名在展示广告的页面上，Training 和 Agent 默认阻止，Search 默认允许。一个爬虫如果同时承担 Search 和 Training，会按所有行为中更严格的规则处理；站长可以在设置里退出这次默认变更。7

这套分类比一个笼统的「AI bot」开关更可操作，却把搜索流量依赖直接摆到了台面上。HN 评论里有人支持区分索引、实时代理和训练，另一边担心多用途的 Googlebot、Applebot 或 Bingbot 会让站点陷入二选一：拒绝训练，也可能误伤搜索。还有人指出，robots.txt 长期依赖爬虫自律，AI 爬虫带来的内容再分发和商业竞争让这套「荣誉系统」越来越不够用。2

意图分类之后，新的硬问题是：谁来证明爬虫说的意图是真的？如果三类流量仍由同一身份和请求路径混在一起，分类可能只是控制台上的标签。

3. Debian：争论的中心是责任如何落到贡献者身上

Debian 页面显示，关于 LLM 使用的 General Resolution 在 2026 年 7 月 24 日进入讨论期，页面列出 A、B、C、D 四份提案。Proposal A 要求禁止使用或借助 LLM 生成的 Debian 贡献；Proposal B 允许 AI-assisted contributions，但要求贡献者承担技术、安全、许可证和实用性责任，显著使用时披露，批量变更接受人类监督，且不能把敏感或非公开信息传给不受信任的工具。8

Proposal C 采取「尽可能拒绝」的方向，要求披露并允许维护者完全禁止 LLM 贡献；Proposal D 不主张全面禁止，而是要求 DFSG 合规、本人理解并提交工作、保留责任和适当标记。四份提案都还不是最终决议，不能写成 Debian 已经通过的统一政策。8

HN 讨论把执行难题说得很具体：让 Claude Code 找 bug、提出修复建议，但由人类编辑文件并运行测试，算不算 assistance？如果规则靠自我披露，又怎样验证？另一组评论认为，LLM 用于代码分析和漏洞发现已经是现实工具，禁止它可能拖慢安全修复；应该固定的是理解、审阅和签署责任，而非某个工具的名称。3

社区规则面对生成工具，不能只写「允许」或「禁止」。生成、分析、翻译、批量修改、披露和责任如果没有定义，纸面上很严格，落地时却只剩下猜测贡献者有没有说实话。

4. Ruff：默认检查项其实是一份迁移政策

Astral 在 2026 年 7 月 23 日发布 Ruff v0.16.0，宣布默认启用 413 条规则，高于此前的 59 条。Ruff 说，新默认集合包含能发现语法错误和直接运行时错误的规则；想恢复旧默认集合的用户，可以显式选择 E4、E7、E9 和 F。9

对新项目，这是省配置的体验。对旧项目，它更像一次迁移政策：升级工具就会得到一批此前没有出现的诊断。HN 评论里有人说 413 条规则能让 agentic coding 更有约束，也有人在自己的代码库里遇到上百个无法自动修复的问题，担心为了清空警告而引入例外、改坏可读性，甚至让 agent 为了通过检查而做出错误选择。4

Ruff 把规则放进默认值，换来的不是单纯的质量提升，而是更低的发现成本和更高的升级责任。--fix 能改文件，不能替团队决定哪些约束值得保留。

5. Lean：自动化可以补证明，但不能替人提出问题

ImperialViolet 博客作者在 2026 年 7 月 26 日发表文章，尝试用 Lean 写一个 Zstandard 解压器，并用定理说明 FSE 表构造的大小、符号分布、状态范围和可达性。文章把这些内容描述成优化解码循环所依赖的隐含前提：在普通语言里，它们可能只是一段注释或测试；在 Lean 里，它们成为类型和证明器可以检查的条件。10

作者认为，LLM 加上证明不可相关性，可能降低依赖类型系统的证明成本。HN 的三条评论没有把它当成自动获得正确性的捷径：有人认为人仍要选择合适的证明目标和分解方式，否则模型会绕开真正的 proof obligation；也有人提醒，模型可以帮助搜索证明，但不能替人确认规格是否表达了原本的意图。5

这和 Ruff 的自动修复形成对照。前者生成代码修改，后者生成能否满足明确不变量的证据。两者都依赖人先把问题切对：没有清楚的规则，自动化只能更快地处理一个不清楚的目标。

规则写进机器以后，谁获得了选择权

把五条帖子放在一起，可以看到规则逐层变得更具体：

信号层：浏览器替用户表达隐私偏好，但需要制度或平台让信号真正生效。
分类层：Cloudflare 让爬虫声明用途，但还要验证 Search、Agent 和 Training 的身份与行为是否一致。
政策层：Debian 把工具使用放进贡献流程，同时处理披露、责任、许可和隐私。
默认层：Ruff 用一次升级改变大量项目的检查面，因此默认值本身就是版本兼容和迁移政策。
证明层：Lean 把代码中容易被忘记的前提变成可检查的工件，但前提仍由人选择和解释。

这五层不能互相替代。浏览器有隐私信号，不代表网站会遵守；爬虫有用途分类，不代表站长能验证；Debian 有披露规则，不代表它天然可执行；Ruff 有更多规则，不代表每个警告都值得修；Lean 能检查定理，也不代表定理就是正确的产品规格。

对做软件的人，今天热榜留下的检查清单很实际：规则由谁写，机器如何读取，误判由谁承担，升级如何回退，用户能否退出，最后又有没有一份能被别人复核的证据。把规则写进接口，确实能减少含糊的口头约定；同时，它也会把原来藏在「默认如此」里的权力和成本，一项项摆到明面上。

从 Cookie 信号到 Lean 证明，软件正在把规则写进机器