把代码库调教得更适合 Agent：类型反馈、Expect Test，以及正式方法新账本
@poteto 推荐的 @yminsky 这场 Bug Bash 演讲，并点出几条她认为最值得带走的实战经验，用来把代码库本身改造成更利于 Agent 工作的环境，一起看看。
https://www.youtube.com/watch?v=rUYP4C29yCw
Agent 让写代码变便宜之后，Jane Street 的立场并不是「少做工程」，是：类型、测试、code review 这些老本事变得更重要、也更要换形态，它们给模型提供快反馈与全局不变量，给人提供可读的行为痕迹与理解；目标是放大人的杠杆与理解，不是消灭人写/读代码。正式方法从「贵到几乎不用」开始变成值得下注的方向。
Jane Street 是怎样的工程现场
全球交易公司：200+ 交易场所、约 3500 人（约 2000 人日常写代码）；体量上自述约占美股约 10%、美期权约 8%、欧洲 ETF 约 20%，日交易规模到数千亿美元级。工程上强调：正确性要按代价敏感地分配精力；重度采用 AI agent（曾长期「净拖累」，约去年 11 月模型跨过门槛后采用陡升）；自研交易用 ML；主语言 OCaml（含自家扩展 OxCaml），ML/脚本用 Python。领导开发者工具的人常说：我们都是 AI assistant 了，做工程工具若不把 agent 层算进去，就是没做完本职。
开场自嘲像「过气老登」：世界剧变，却更坚定地主张「以前那些道理，现在更该做」。
类型：不只是管子对不对，更是设计与全局不变量
类型系统开箱消灭整类错误（无隐式 null、越界等）；自家扩展还有类型安全栈分配、数据竞争预防。更关键的跃迁是：把类型从「保姆」变成设计工具，表达、强制、结构化应用不变量。
例子：
· XSS / 注入：用类型强制 node.text 等转义路径，漏写即类型错；价值在「隔空作用」，错误可发生在多层调用任一处，类型把全局不变量拴死。
· Make illegal states unrepresentable：网络交换机配置从「命令序列变体」改成记录字段（0/1 次用 option，多次用 list），算 MTU / shutdown 的代码更短，也不再有「说两次 shutdown / 取第一个 MTU」的语义含糊。
Agent 时代为何更需要类型
Agent 靠反馈活着（推理时与训练时皆然）。类型错误是按需、极快的上下文；比测试套件更快，利于 harness 效率。模型随机、记忆有界，230k token 后可能忘了你要求怎么调构建工具，更难自觉维护横切不变量。把结构写入类型，等于给模型可看见的严谨骨架；小而精的 typed kernel 可在全仓强制规则。验证正成为瓶颈，类型也帮人读懂正在造的系统。
测试：Expect test + 库级确定性仿真
他们什么都做：单测、QuickCheck 属性测、AFL fuzz、全系统确定性仿真（含 Antithesis）、prod/dev 并跑、历史回放等。重点推销的「怪招」是 expect test：跑一段代码，把打印输出嵌进源码；失败时是与期望输出的 diff，可一键接受。
听起来像懒，不先想性质、只看输出像不像。但他们的主张是：做得好时，expect test 是驱动人对系统理解的工具。输出必须刻意做成人类可读（甚至给硬件工程师做「纯文本示波器」）；胡乱 dump 则无意义。
配合库级确定性仿真（mock 网络、时钟、服务发现）：反馈可到毫秒级，而非分钟/小时。可把 client / proxy / server 缠在一起看轨迹，例如服务发现要几秒才第一次广播，导致「客户端为何 5 秒才连上」变得一目了然。
为「基于例子」的测试辩护：软件多数脆，错一点就错一大片，因此少量精心挑选的触点往往有效；类型带来的 ∀ 让系统更易「咔嗒卡位」。人要判断该按哪里（含对实现软肋的了解，而不只接口）；提交进仓的例子还承载意图，有人认为这段行为值得写下来。
对 agent：expect test 是又一个闭环，看见行为与行为变化；文本轨迹比纯视觉对模型更友好；人审 agent 改动时，可读「逻辑 diff + 诱发的行为轨迹 diff」（类比 Excel：程序看紧凑逻辑难看数据流，表格相反；expect 两者兼得）。迭代速度对人与 agent 同样关键。
Code review：在「结束之前」先说清它是干什么的
早期他以为 review 主要防亏钱；实际还包括：传播最佳实践、抬高 bus factor、逼作者为读者写简单代码、对抗组织变大后的「交叉项」拖垮人均产出，以及让代码库可被愉快阅读（留人的一部分）。
Agent 之后为何更重要（至少在当前地平线）
Agent 在整洁、简单、照料好的仓里更好用。Anthropic 多智能体写 C 编译器的 stunt：印象深刻但有缺口（如无类型系统）；更有教益的是怎么结束的，继续改更容易破坏已有部分，前进停滞。脏仓里 agent 也容易陷入同样局面。
Agent 被训成「赢电子游戏」：拼命把红灯变绿，擅长完成你说的功能目标，不擅长维持非功能属性（简单、可扩展、少脚枪、少重复与硬编码）。它们依赖这些属性，却拙于保全，因此 review 至少在当下更关键。人的稀缺工作是理解系统、确认做对且做得好看。
审 agent 代码特别难：
· 社交契约破裂：从前同事投入了时间，你愿优先审；现在有人 YOLO 一句「让 agent 修」就甩过来，不尊重审阅者时间。
· Agent 不真正从教练中成长（会话结束就忘）；改 skill/文档才持久，日常来回感觉不同。
· 许多人读 AI 代码会走神、眼睛发飘。
· Reward hacking 改变错误形态（删测试让绿灯）；昔日「文笔/味道」信号失灵，LLM 几乎不犯语法错，却不等于正确。
Agent 也能帮 review：更敢做大重构提质；把大功能拆成可审的 stack；写澄清测试；当可对话的「神谕」先磨理解再找人聊；实验过让 agent 设计 walkthrough 顺序降低认知负荷。
正式方法：从「超级不感兴趣」到开始组队
过去对外常泼冷水：喜欢好类型，但对 formal methods 极不感冒。现在成本结构在变，seL4 量级仍极贵（约 8700 行 C、约 25 人年、约 23 行证明/行 C），但数学侧（IMO/Putnam、Terry Tao 与 Lean 结对）显示：agent 未必比顶尖数学家更「聪明」，却背过互联网、极熟工具，能把领域专长与证明工程专长嫁接。这仍是赌注，当前模型未必够强，但值得加大投入。
方向举例：refinement types（读好写难 → 或许让 LLM 写标注）；差分验证（「这次 diff 对下列性质是 no-op」）；从简单纯函数参考实现到复杂命令式实现的等价证明；语言设计互动（如 Rust/Verus 因所有权少用分离逻辑）。约八周前才认真转向，正准备招人建 formal methods 团队。
总原则
反对「人不写不读代码」当目标；应追求人尽可能有效。稀缺资源仍是人的注意力，工具与流程应最大化个人杠杆，既提高 agent 效率，也提高人对系统的理解（后一块谈得不够多）。
Q&A 要点（浓缩）
自动化 code review：支持所谓 AI review（含全仓坏味道审计），但那是 harness 工程；真正的 code review 是驱动人理解，两件事别混。
Dependent types：旧我怀疑性价比；新我因 agent 改变成本曲线而更感兴趣，但仍看重类型系统甜区与人体工程学（例：local mode 做栈纪律与 capability，防 web 框架「建图阶段 / 运行阶段」混用）。
可验证性是否逼你改设计：成功图景应是加速而非拖慢；许多未为验证而设计的程序本身就不正确，难证伪命题。看好「人写简单意图实现 + agent 做快实现与证明」。
代码风格 vs 文风：代码要中性、可共享；散文仍要人味与社会契约。LLM 很会模仿仓内风格（有时连坏风格一起学），这点他反而放心了。