## 正式验证 50 年进展 (1975-2025) 最近关于科学停滞的说法忽视了计算机领域的进步,尤其是在正式验证方面——对软件和硬件正确性的严格证明。虽然早期的计算进步受益于工业研究,但基础工作源于学术界和政府资助。本文重点介绍过去 50 年证明助手的发展,从 1975 年的爱丁堡 LCF 开始,该系统通过严格的推理规则确保定理生成。 剑桥 LCF 紧随其后,为 HOL 系统家族铺平了道路。Isabelle 于 1986 年出现,支持构造类型理论并能够进行复杂的形式化。20 世纪 90 年代的一个转折点是 John Harrison 对浮点算术的验证,展示了这些工具在严肃数学方面的强大功能。 21 世纪见证了越来越多的采用。里程碑式的成就包括 ARM6 处理器的形式化验证、CompCert 编译器以及亚马逊网络服务 (AWS) 的 Nitro 隔离引擎,使用了 26 万行 Isabelle/HOL 代码。数学家越来越多地使用 Lean 等证明助手,例如对主要定理的形式化以及对确认新数学发现的贡献。正式验证正从一个利基领域转变为可靠系统开发的关键组成部分,证明进展*正在*进行。
## OpenAI 拥抱“技能”概念
OpenAI 正在迅速采用 Anthropic 首创的“技能”机制,使 LLM 能够利用外部工具和知识。这种系统,仅仅是一个包含 Markdown 指令和资源的文件夹,已经悄然出现在 ChatGPT 的代码解释器和 Codex CLI 工具中。
在 ChatGPT 中,技能目前支持电子表格、DOCX 文件和 PDF(渲染为图像以保留布局)。最近的测试表明,ChatGPT 成功创建了一份 PDF,总结了 rimu 树对 kakapo 繁殖的影响,展示了其研究和格式化信息的能力。
Codex CLI 也获得了实验性的技能支持,允许用户安装自定义技能——例如,用于创建 Datasette 插件的一个技能——并相应地执行任务。这使得强大的代码生成和自动化成为可能。
作者认为,技能代表了 LLM 能力的重大进步,超越了多轮提示 (MCP) 的影响。他们建议正式记录技能规范,这可能成为 Agentic AI Foundation 的一个项目。
## 将 Go 带入 Python 世界 & 优化 Docker 构建
作者的任务是在主要使用 Python 的公司环境中构建第一个 Go 服务。选择 Go 是因为它速度快、易于使用,并且是 Rust 或 Nix 的舒适替代方案。该项目涉及一个远程代码执行 (RCE) 服务,Go 的安全特性是关键考虑因素。
最初,作者尝试使用 Nix 进行镜像构建,但由于团队已经熟悉,最终回到了 Docker 和 Docker Compose,尽管承认他们当前的 Docker 工作流程效率低下。文章详细介绍了优化 Docker 镜像大小和构建时间的努力。
关键技术包括使用 `scratch` 或 `alpine` 基本镜像进行多阶段构建,利用构建参数 (`CGO_ENABLED=0`) 进行静态编译,以及使用绑定/缓存挂载以加快依赖管理。`.dockerignore` 文件对于排除构建上下文中的不必要文件至关重要。还优化了图层顺序以最大化缓存。最终,作者实现了仅 15.9MB 的最终镜像大小,证明了通过这些 Docker 优化策略取得了显著改进。