ezyang：用编程语言本身当规格语言，编译正确性也进了 TCB
ezyang · x · 2026-11-09
ezyang 提出：假设你喜欢的语言有形式语义，可以绕开专用规格语言、直接复用原语言写性质——例如 Anthropic 文中把性质写成「不许崩溃的 fuzz test 程序」。但代价是：规格语言希望 TCB 尽量小，而一旦依赖编译输出的底层语义，编译器对规格的正确编译就也被拖进了 TCB。
所属事件:Anthropic 汇编级形式验证引热议，ezyang 追问 TCB(6 条相关)→
「编程与Agent」频道最新
- AI Agent 一个周末修完 41 个报告问题中的 40 个 — julianweisser · 2026-11-09
- HEELO 框架让 Terminal-Bench 解题率从 37.3% 升至 55.5% — Haibo Jin · 2026-11-09
- NVIDIA 研究:得当时机的强弱模型交接可大幅省 Agent 成本 — nvidia · 2026-11-09
- FrontierCS 榜单更新：Claude Sonnet 5.5 在 50% 任务上超参考解 — ajratner · 2026-11-09
- 「会技术」新定义：有耐心反复问 Claude 直到搞懂为止 — brandon_galang · 2026-11-09
- Together AI:榜单只能选入围名单,真正该测的是你自己的流量 — togethercompute · 2026-11-09