测试，而非(仅)验证
我理解其吸引力，欣赏这个构想，也信任研发这些系统的研究者，但对那些宏大的承诺并不完全认同。
人工智能正推动形式化验证走向主流。
人工智能辅助机械证明公司正以数十亿美元估值融资，新用户正以空前速度尝试证明助手——其中绝大多数采用精益模式。在国际数学奥林匹克竞赛、国际大学生程序设计竞赛、普特南数学竞赛等曾被视为全球最难竞赛中，模型取得了惊人成果；在数学领域，诸如埃尔德什问题等悬而未决的难题也正被攻克。不仅业余爱好者对人工智能辅助证明充满热情，从陶哲轩到马丁·克莱普曼到伊利亚·谢尔盖，全球顶尖研究者都对这项技术的效果充满期待与希望。
形式化验证的价值
容我简要阐述核心论点：
形式化验证面临多重复杂挑战。首要难题——也是技术层面最难攻克的——在于全球绝大多数软件缺乏形式化规范。所谓形式化规范，是对所构建系统进行简化的数学描述。算法、数据结构、协议、数据格式以及安全关键系统通常都具备形式化规范。然而现实中，绝大多数程序既没有形式化规范，甚至连非正式规范都付之阙如。在我们当前所处的极限状态下，程序的规格说明就是程序本身，实现即规格。缺乏形式化规格使得软件的正式验证极其困难——毕竟你究竟要验证什么？
第二个问题在于证明工程的实践难度极高，即为系统相关定理编写证明的过程。证明中存在大量领域特异性元素：数学定理的证明与编程语言的证明截然不同，而后者又高度依赖其理论框架的基础构造。最广泛使用的证明工程教材是《软件基础》，其中每个章节的证明风格都各不相同。研读过第二卷《编程语言基础》的读者，往往难以直观理解第六卷《分离逻辑基础》中的问题。此外还存在证明自动化工具的局限性、证明的脆弱性、证明复用性等问题，但我认为这些并非证明工程本身的根本性缺陷，而是当前技术阶段的产物，暂且搁置不议。
大型语言模型在编程领域的崛起对上述两点产生深远影响。其影响点一在于：人工智能辅助编程与规范驱动开发天然契合。这种编程方式将编程边界从“可实现”拓展至“可规范”与“可验证”。这极大激励了可执行规格的编写，因为此时可将LLM置于循环中持续迭代直至达成目标，且不拘实现手段。我预测这将催生革命性的程序优化器与翻译器，彻底改变相关领域的工作模式。然而测试本身存在众所周知的缺陷——它们永远不完整。测试虽擅长发现缺陷(实际上多数时候效果并不理想，但这另当别论)，却 无法 证明系统无缺陷。SQLite虽拥有数百万测试用例，研究人员仍能发现其漏洞，类似情况几乎存在于所有软件中。
唯一能证明无缺陷的方法是形式化验证，产业界已涌现诸多成功案例。高引用率的形式化验证项目包括CompCert C编译器——其针对GCC和Clang的随机测试发现GCC存在79个漏洞，Clang存在202个漏洞，而CompCert在未验证的解析器中仅发现2个漏洞，其验证过的编译阶段则未发现任何漏洞——这无疑是形式验证的重大胜利。(感谢A. Jesse Jiryu Davis告知，我了解到研究人员已研究过形式化验证分布式系统中的故障根源，发现对系统未验证部分的错误假设很可能是罪魁祸首。)
这使得形式化验证成为人工智能辅助编程的首要目标。既然我们拥有形式化规范，便可让机器持续运行数小时、数日甚至数周。若最终获得解决方案，我们信任的并非所谓人工智能的概率预测，而是验证该解法的符号证明检查器。这一理念始终是形式化验证的核心——不健全的证明生成与健全的证明检查相结合，催生出复杂的战术策略，即通过搜索生成证明的算法，从而赋予证明工程师强大的能力。
好消息不止于此。人工智能在撰写证明方面同样表现优异，至少远胜于普通软件工程师。假设存在完美预言者，我们还能将问题转化为RLVR(可验证奖励强化学习)，这意味着随着时间推移，模型将如同在国际象棋、围棋等领域那样持续提升其证明能力。这正是其估值达数十亿美元的根基所在：初创企业凭借出色的自动形式化技术和自动证明器攻克竞赛难题与开放猜想，但真正的工业价值在于软件工程核心的自动化——工程师只需撰写文字描述，系统自动将其形式化为精简定理，经自动证明器验证后，即可获得完全可信的程序。
但我们真的能做到吗？
形式化验证：弊端篇
我理解其吸引力，欣赏这个构想，也信任研发这些系统的研究者，但对那些宏大的承诺并不完全认同。本文试图通过阐述优点(如前所述)与弊端(下文将论述)，在合理的中间立场上构建平衡观点，并重申测试在当前及未来领域中的定位作为结语。
自动形式化是块不稳的基石
开篇我指出全球多数程序缺乏形式化规范，随后阐述了人工智能如何激励我们编写规范，而自动形式化正是将这些规范转化为 形式化 的工具。在形式化验证领域存在*可信计算基(TCB)*的概念。TCB如同阿喀琉斯之踵，是验证体系的基石——层层验证都建立在此之上，我们默认信任这个核心组件而不作验证，因为验证体系必须有根基，无法构建自证循环论证，系统也无法自我验证。(若此处有误，请务必核查，此可能性确实存在)
在AI辅助验证编程范式中，自动形式化属于TCB范畴，因为无法机械验证口头描述的规格是否确实对应形式化规格。其使用模式存在多个问题，其中之一是可靠性——某些经机械验证的场景可能被口头规格所拒绝。另一问题在于完备性——形式化模型可能拒绝我们描述中的有效场景。自动形式化环节需要并值得我们特别关注，因其是验证流程中的关键失败点之一。
证明助手运行缓慢
在证明助手(proof assistant)中，核心目标是实现程序推理与简化验证流程。例如传统证明助手不采用内存中经典的字节封装二进制补码整数，而是使用皮亚诺数——一种将自然数编码为归纳数据结构的方案：
Inductive Nat : Type :=
| zero : Nat
| succ : Nat -> Nat.
这种编码不存在整数溢出的概念。其归纳结构使我们能够构建适用于所有自然数的定理，而不仅限于能容纳在一个字中的数值。它还极其缓慢——a + b的计算复杂度高达O(a + b)，这项在CPU中本应瞬间完成的运算，其时间复杂度竟与加数值呈线性关系，而非常数级操作。然而我们需要在实际工作负载中运行经过验证的代码，因此无法等待百万次循环来完成1M + 1M = 2M的运算。对此有两种解决方案：其一是构建更高效的编码方案，在证明助手中证明高效但难以推理的编码与低效但易于推理的编码等价，并在计算中采用高效方案。另一种方案仍是公理化，即扩展TCB(类型控制边界)。证明助手提供名为 提取 的机制，可将证明助手语言(如Rocq)中的代码片段提取至生态更完善的生产级语言(如OCaml)。大部分提取过程通过语法转换实现语言间的一一对应，但我们可以劫持提取机制来自行公理化类型系统。例如将Nat转换为无符号整数，此时Nat.add即变为u64 + u64。例如在Rocq中，Nat会被提取为BigInt，二者应具有相同语义——但此处的“应”字承载着沉重责任。若缺乏配套的正确性证明，我们只能将BigInt纳入信任基础(TCB)。
若不扩展TCB，证明助手的速度将受限于大量指针追踪操作，这种操作因归纳类型的使用及其树状特性而自然产生。在许多领域中速度并非首要考量，但我认为速度与正确性要求之间存在矛盾：更快的代码往往涉及更复杂的语言构造(如并发、位操作、布局感知)，这些构造比简单对应物更易引发错误。若我们无法对更易出错的程序进行推理，那么我们究竟解决了多少根本性问题？
验证需要模型，而模型极其稀缺
要验证系统的某个属性，就需要系统的模型。这些模型并非唾手可得，而是领域专家历经数年精心构建的成果。人们已为指针程序(分离逻辑)、并发程序、随机程序、代数效应程序等构建了模型，或许还有许多我未曾听闻的类型。在证明系统属性时，我们需要推理过程的基础支撑，而这些理论恰恰为各自领域提供了这样的基础。然而许多领域尚缺乏完善模型，运行时性能便是典型例证。这在计算机科学课程中始终存在争议——渐近复杂度无法直接映射到真实硬件中的程序行为。现代CPU具备缓存行、投机执行、分支预测等特性，使得渐近分析中使用的传统抽象机器在多数场景下已然过时。我们甚至无法找到单一硬件来验证模型，面对数十种硬件配置时，每种配置都会导致测量结果差异。若试图证明某段代码在特定内存/处理器组合中优于其他代码，将面临艰巨任务——我个人甚至不知从何着手。
反观测试环节，只需在两台机器上运行相同算法并执行基准测试，最终结果即为基准实证。测试虽普遍被视为弱于形式化验证——当资源不足以支撑验证时才会采用——但若能投入时间证明系统无缺陷或验证普适性事实，其价值远胜于将单次测量结果固化为代码。我要强调的是：某些测试方案无法通过形式化验证实现——尽管构建验证模型可能困难重重，但直接使用真实硬件进行测量往往更为简便。
验证无法指出你是否走错了方向
在游戏中，胜负分明。而在验证领域，你可以证明定理正确，也能证明定理错误，但缺乏证明并不意味着定理错误——或许你只是尚未找到证明。这意味着撰写证明时获得的反馈有限：你无法将论证受阻视为定理错误的信号，因为问题可能出在你自身。正因如此，QuickChick——这款源自Haskell著名工具QuickCheck(它向世界引入了属性驱动测试)的测试工具，在Rocq生态系统中成为三大热门包之一。若验证严格优于测试，QuickChick便无存在必要，但它承担着验证流程中至关重要的角色： 证伪 。我曾指出：缺乏证明并不意味着定理错误，但定理被违背的实证则绝对如此。随机测试正是发现此类反例的首要手段，它能将验证器从证明搜索的兔子洞中拉出——避免验证器在证明搜索中徒劳地遍历无数无用路径后最终放弃，因为定理本身终究是错误的，根本不存在可被发现的证明。
随机测试与形式验证
我已举例说明形式验证无法建模的测试场景，以及通过创建短程序来反驳错误定理(而非徒劳地证明它们)从而补充形式验证流程的测试案例。测试与形式验证的协同效应不止于此。我坚定支持验证引导开发(VGD)，该方法不仅强化这种协同，更能解决证明助手运行缓慢的问题。在验证引导开发中，我们实现同一系统的两个版本：一个是更易推理的验证版本，另一个是复杂的生产版本。通过让生产系统与经过验证的参考实现运行相同输入，并断言每次结果完全一致，我们验证了生产系统符合规范。VGD利用差异随机测试技术，将证明从证明助手实现的低效版本“提升”至生产实现，从而构建出兼具正确性与高效性的两全其美系统。下图摘自论文——据我所知该论文首次提出VGD概念，图中阐释了其工作流程。
VGD虽未能解决本文后续提及的所有问题，但它消除了系统中的低效环节。随着生产级实现方案已准备就绪，我们可开展各种超出验证范畴、属于测试范畴的测量工作。这使经过验证的计算领域与未验证领域处于平等竞争环境，从而降低了验证利用测试带来的弊端。
结语
在此再次向各位重申：
我理解其吸引力，欣赏这一理念，也信任研发这些系统的研究者，但对其宏大承诺持保留态度。本文旨在通过剖析利弊构建合理的中间立场，并通过重申测试在当前及未来领域的地位来作结。
我坚信随机测试在软件工程未来的发展中，与形式化验证同样重要。许多领域不会凭空出现形式化验证系统，但随着自动形式化工具的进步，我们将拥有更多形式化规范。随机测试与形式化验证虽以不同方式受益于这些规范，但二者各有其位。缺乏配套测试工具的证明系统终将残缺，而缺少正确性证明的测试工具同样不完整。唯有通过验证与测试的有机结合，我们才能实现软件工程的未来愿景：让缺陷成为异常而非常态，使正确性成为美德，让系统中的漏洞如同人类已治愈的疾病般古老而被遗忘。
本文由 TecHug 分享，英文原文及文中图片来自 Test, don't (just) verify.。
本文低估了近几年数学证明形式化领域取得的成就，以及该领域距离最终解决目标的接近程度。
若暂且抛开编程领域，仅聚焦数学形式化(克里斯蒂安·塞格迪在此领域深耕已久)，当前可形式化的证明长度正呈指数级增长。2026年人类撰写的大型/重要证明几乎全部能被Lean系统翻译并验证的可能性极高。
以编程/建模缓存行和周期计数为例：我们已为众多架构建立了相当完善的模型(某些论文中甚至包含针对NVIDIA GPU的精确逆向工程模型)。问题在于计算缓存读写的确切数值极其枯燥——其中包含大量常数，且每次微调模型都需重新计算。
这涉及大量枯燥的约束条件求解，而我手动处理时的核心瓶颈在于无法完全信任大型语言模型的输出结果。
我认为这忽略了学习验证的重要性所在。例如学习不变量及其类型(如循环不变量)的概念，能显著简化代码推理过程——即便不进行正式验证，也能更轻松地编写测试或断言()。大量缺陷源于程序状态与程序员预设状态不符，而现有工具正致力于解决此类问题。例如静态类型语言本身就是一种验证机制——它验证变量类型及其可操作性，并限制函数的有效输入输出范围。像Rust这样的语言在内存正确性方面也具备验证功能，同样是极其有用的工具。
“谨防上述代码中的漏洞；我仅证明其正确性，未实际测试。”——唐纳德·克努特
此语在此语境下关联性不强，因该代码用于完成形式化证明，而非证明工具本身。不过在讨论软件验证时，这句名言确实广为流传——毕竟总得有人来做这件事…
上下文：https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf
在着手编写Lean之前，或许我们该先从Rust这类“更笨拙”的类型化语言起步。若追求程序正确性，动态语言绝非良选。类型检查是最实用且广泛运用的测试手段。
类型错误——尤其当类型设计本身就确保正确性时——对大型语言模型极具价值。当基础架构正确无误，模型只需在狭窄缝隙中反复尝试，终将找到契合的解决方案。
但根据我目前的理解和阅读，我对楼主所谓的“形式化验证”并不信服。一个简单的试金石是：选取你近期工作中任何一项任务，尝试为其描述形式化规范。这是否可行？是否合理？是否存在？对我而言最有价值的验证是针对底层工具的验证，即数据结构、语言、编译器等。
例如Rust中Vec::operator[usize]的类型签名返回T，这显然不成立——它无法保证对任意usize值都返回T。在我看来，panic是实现规范最懒惰且最糟糕的方式，它意味着每行Rust代码都可能进入终止状态。
我曾听过一位在node.js领域颇具影响力的演讲者开场白：“静态类型检查只是单元测试的替代品。”
我当时真想朝他扔鞋。静态类型检查并非替代“某个”单元测试，而是替代了无数个单元测试。
换言之，JavaScript和Python用户普遍存在这种误解：认为单元测试与类型检查效果相当(且更灵活)，这本质上混淆了“存在”与“全称”这两个逻辑运算符。
况且设计程序类型本身就比编写单元测试更有趣。这种乐趣源于更高层次的抽象操作，它能激发大脑更强的解谜模式，远非单纯编写单元测试可比。迫使自己思考“对所有x成立”而非具体x，能让大脑深入考量所用x的属性。
> 设计程序中的类型比编写单元测试更有趣。
我两者都尝试过，完全不明白你在说什么。
> 迫使自己思考“对于所有x”而非具体x，能让大脑深入考量所用x的属性。
动态类型的核心价值在于，它让你能够关注接口而非具体类型，这要求你深入思考对象的属性(即所提供接口的语义)。
这并非动态类型的全部意义，因为所有接口概念都源自静态类型语言。部分*动态语言借鉴了这些概念，但多数采用“隐式”接口——我猜这种接口就是“能凑合用”的类型。
> 因为所有接口概念都源自静态类型语言。
不，并非如此。它源于语言诞生之后的理论。
> 部分动态语言借鉴了这种设计，但多数采用“隐式”接口
隐式接口本质上仍是接口，恰恰是我在泛泛而谈中讨论的类型。关键在于你应从对象的能力角度思考，而非预先验证的分类框架。关注对象做什么，而非是什么。
通过结构子类型化(如Go接口和Python协议)可实现此目标。但其优劣则是另一问题。
> “静态类型检查只是单元测试的替代品。”
这并非新论点。Rich Hickey早在2011年《简单即易》演讲中就提出类似观点，不过他着重指出：软件系统中最易出现的缺陷往往能同时逃过类型检查器和测试套件的双重把关。更早之前，Python和Ruby社区也曾流传过“测试套件可替代类型检查器”的类似理念。
我清楚记得“测试使静态类型检查变得多余”的观点在JavaScript社区曾盛行一时，导致TypeScript在最初三四年间推广异常艰难。直到2015年Visual Studio Code问世，并逐步在Atom和SublimeText中抢占市场份额，才让更多人接触到TypeScript及其类型检查器的优势。总体而言，TypeScript耗时近十年才成为Web项目的“默认”语言。
赞同。
况且动态类型语言中类型并非无关紧要。合格的程序员编程时仍需在脑中保持类型意识：“这个函数能处理浮点数吗？还是必须传入整数？” “该函数要求可迭代对象，但若传入字符串会怎样？”等等。
我职业生涯起步于JavaScript和Python，但多年实践让我确信：那些向程序员隐藏类型、在后台进行隐式转换的语言并不能提供更好的开发体验。它们或许能降低初始学习门槛，快速原型化的理念也颇具吸引力，但很快就会引发维护难题和大量漏洞。在 Python 的类型提示工具流行之前，我参与的许多项目中，
TypeError都是 Sentry 异常统计里遥遥领先的头号问题。渐进式可选类型比完全没有强，但根据我的经验，如果语言不强制要求，大多数程序员会偷懒，只做最低限度的类型声明。特别是像 TypeScript 这样的方案，让许多声明变得难以阅读、编写和理解。
我认为类型推断是稳妥的中间方案。类型依然通过静态声明，但编译器足够智能，在类型显而易见时不会打扰开发者。
> 在 Python 类型提示工具流行之前，我参与的许多项目中，
TypeError始终以压倒性优势占据 Sentry 异常榜首。我的经历截然不同。在未注释的Python代码中，
ValueError异常更为常见，而TypeError最常见的根源往往是重构后参数顺序或数量错误。嗯…我可能记不清是
ValueError还是TypeError了，毕竟已是几年前的事。但可以肯定的是，在所有我参与的Python项目中，类型问题始终是最频繁出现的。你的经历为何不同？
数百个单元测试可替代类型声明。
启用属性机制后，测试量将飙升至数千。
绝大多数代码都应采用类型化设计。Python虽适合原型开发，但原型成型后必须引入类型系统。
我向来厌恶Python，完全无法享受它。其开发体验与PHP、JavaScript、Ruby等语言同样糟糕。
终于在neovim里配置好pyright；给每个该死的元素都加了类型，现在我爱上Python了[1]。
迫不及待想看到TC39落地(其实上周才在HN上了解到这个)。说不定我也会喜欢上JavaScript。
——————–
[1] 当然要讲究分寸；打包体验依然糟糕透顶！
没看懂TC39这段——它只是个小组，和JS的类型系统毫无关系。
抱歉，我应该更明确说明讨论的是哪个提案：
https://github.com/tc39/proposal-type-annotations
我从未见过Python中正确使用类型的情况。
元组甚至不算类型！它只是类型构造器！我专业从事Python和TypeScript开发已有近二十年(Python)和五年(TypeScript)，可以非常肯定地说这无关紧要。
况且你似乎混淆了Python运行时与类型检查时——理论上虽有遗憾，但实践中仍是无关紧要的区分。(不幸在于Python类型检查本质上与Python执行是两种不同的语言；无关紧要在于两者的正确子集能很好地对齐。)
你在Python对象模型中试图区分的概念毫无意义。类型本质上可调用，调用它们会构造(即实例化)类型(通常如此；设计上可覆盖此行为)。也不存在类型→种类→类别的层级关系；
type本身就是一个对象，拥有自己的类型。当理论层面出现“类型构造器”这类术语时，就没法指望这些概念适用于Python了。这就是为什么Haskell开发者将Python这类动态类型语言统称为“无类型”——无论他们对隐式转换持何种态度。
而我深爱这种设计，数十年来持续使用它，编写出优雅的代码——其中类型注解几乎不值得费心(或许用于文档，但绝非静态检查器所需)。再看看其他新晋Python开发者，他们费尽心思编写复杂泛型类型表达式(为追赶Python迭代提供的注解语法而牺牲向后兼容性)，还要处理协变与逆变等难题，我只能莞尔。
大多数类型“甚至算不上真正的类型”。正因如此，你才能将类型(而非字符串)作为值传递给函数。
若类型是真正的类型，你就无法将其作为值使用。
单元测试是功能性断言。类型作为语义构造能实现此功能，但它提供的远不止于此。
举个简单例子：若我创建“string”到“foobarId”的类型别名，在符合规范的语言中，就能防止使用foobarId的代码误用字符串。
Python支持类型真是太好了
Python将魔法注释形式化了。
你可以用第三方代码检查工具扫描这些注释，但必须祈祷它们正确无误。通常会有一些检查机制，但仅在简单场景下可靠。
这与静态类型无关，正如“用emscripten将JavaScript转译为C语言”不能证明JavaScript是支持原生汇编的底层语言。相较于“毫无系统可言”的状态，这已是巨大进步，我为其存在感到振奋，但两者本质截然不同。
这些注释最初属于非正式化的魔术注释。该特性原名注解(annotations)，本质上可承载任意内容。
TypeScript的成功促使众多动态语言转向渐进式类型系统，这现象本身就值得玩味。
Erlang和Clojure是先行者，TypeScript紧随其后，如今Python、Ruby甚至Perl都已具备类型声明与程序类型检查机制。
> 那么Python支持类型真是好事
“可选类型”不等同于“静态类型”。
太棒了，我的程序会崩溃，因为我忘了选择启用类型声明 :-/
C语言有void指针。
> C语言有void指针。
那又怎样？void指针并非默认类型 :-/
用Python我得额外努力才能触发类型错误。
用C语言我得额外努力才能隐藏类型错误。
我实在难以理解你的论点。
我认为这恰恰是malloc的精确返回类型。
你必须额外操作才能显式类型化。
我不知道还有哪个静态类型语言会这么做。
希望这能助你理解之战一臂之力。
> 我认为这恰恰是malloc的精确返回类型。
> 你必须额外做工作来显式指定类型。
不。在C中将malloc的返回值强制类型转换是代码异味。若在C++中使用malloc才需要额外工作。
> 希望这能助你一臂之力。
不明白你这句话的含义——难道不是你把C语言扯进Python讨论的吗？
他可能混淆了静态类型和强类型。
C是静态类型语言，但属于弱类型——你需要舍弃类型才能完成许多常规操作。Python是动态类型语言，但属于强类型，当类型无法解析时会直接报错。
C#和C都是静态类型且强类型的语言，不过实践中C#的类型强迫性比C更强。
面对自相矛盾的论点，实在难以辩驳。
但实现得相当糟糕，存在大量边界情况和陷阱，一旦代码调用numpy或处理JSON数据就会让你痛苦不堪。
请详细说明：Python如何使用类型？遗憾的是我如今专业编写Python代码(它确实是拥有所有库的语言)，却对此深恶痛绝。
持续憎恶只会阻碍进步。不必喜欢它，但憎恨会形成心理障碍。
mypy是最简单/最老的选项，也看看pyright和ty。
安装uv后
剩下的就搞定了。
> 我真想朝他扔鞋。
你该扔的！
若在意参数类型，直接在方法里加断言就行 /s
用静态类型来模拟现实世界中常用编程语言的单元测试？祝你好运。先举个简单例子：这些记录应该按出生日期排序。之后再探讨更复杂的情境。
> “记录应按出生日期排序。”
C#的写法有何不妥：
没人声称类型能替代所有单元测试。
它们只是替代了那些平庸的单元测试。
该评论也从未声称类型能替代测试！我认为两者是相互独立的。
该评论明确旨在驳斥“…单元测试与类型检查同样有效”的观点，并指出前者明显逊色。
不。他们反驳的是“静态类型检查只是单元测试的替代品”这一主张。该主张认为只需移除类型检查并替换为单元测试即可无损实现功能。评论指出：为替换单元测试而移除类型检查的做法更差。该状态本身已被预设为存在可替换的类型检查/可类型检查条件。
这恰恰与针对该评论的回应所主张的观点相反——后者声称该评论认为所有单元测试皆可被类型检查取代。这两种主张完全不同。
为更清晰阐明，该评论指出：我曾听过一场宣称“类型检查→单元测试”的演讲，我认为这很荒谬。
回应称：单元测试→类型检查并不合理。因此你所谓“类型检查→单元测试很荒谬”的论断显然错误。
> 静态类型检查不能替代“单个”单元测试；静态类型系统能替代无限数量的单元测试。
你混淆了“单个静态类型检查”与“静态类型系统”的概念。单元测试同样替代了现实世界中无限状态的输入。它们只是被置于试探性验证系统而非证明系统之下。事实证明，编写证明并非多数人的乐趣所在——即便在编程领域亦是如此。况且通常被理解的“类型”概念本身就过于贫乏。
> 换个说法…
此类修辞既缺乏说服力，坦白说还颇具侮辱性。你将个人偏好与观点包装成事实，却未能理解反方论据。
作者身处优越地位，所研发的系统拥有正式规范和经形式验证的参考实现。这篇帖子并非畅想理想状态，而是描述其现有系统(Cedar)的运作机制。
关于你对Rust的论点，绝大多数软件根本无法达到Rust提供的静态保障程度。若需更强保障，请采用静态内存分配——这正是安全关键系统惯用的做法。顺带一提，Rust在内存不足时似乎会终止运行而非抛出异常：https://github.com/rust-lang/rust/issues/43596
我认为用动态语言也能编写正确的系统，只是像Python和JavaScript这类常用语言不行。以Clojure为例，它作为动态语言却相当易于管控，我认为这得益于其不可变特性和数据中心的设计理念。相信还有其他动态语言也能胜任。
当然，我未必会在大型跨组织代码库中使用Clojure(或许可行，但超出我的实践经验)，但它确实能胜任特定任务。
Common Lisp也是如此。虽说不清缘由，但在Common Lisp中我几乎不会遇到类型错误！而JS和Python则常有此困扰。或许有人能解释这种差异感？
我认为关键在于命令式代码和副作用较少，数据转换过程更易追踪。
就像任何随机的JS/PHP应用程序，可能都是由大量循环和if语句堆砌而成。要追踪数据的变化，你需要在脑海中运行整个程序。“现在它把那个属性添加到外部作用域的对象中，接着这个对象被排序，然后它访问数据库…好…” 而在Clojure中，大多数函数要么是对数据集的单次原子操作，要么是一组副作用操作。你依然需要在脑中推演，但可以更分段地进行，不必理解那个充斥着自动加载和变异的类状态、拥有上千个方法的庞然大物。而且你还有REPL环境随时可进行尝试。
别误会，我超爱静态类型。静态类型的Clojure绝对会是史上最牛的语言。但像JS这样的动态语言和Clojure这类语言之间，确实存在着巨大的鸿沟！
> 静态类型的Clojure
若你也钟爱Common Lisp，不妨试试Coalton——这是融合了Haskell式类型系统的Common Lisp：https://coalton-lang.github.io/
> 随便拿个JS/PHP应用看，大概都是堆砌的循环和if语句。要追踪数据流向，你得在脑子里运行整个程序：“现在它把属性加到外层作用域的对象里，接着这个对象被排序，然后触发数据库操作…好…” 而在Clojure中，大多数函数要么是对数据集的单次原子操作，要么是一组副作用操作。你依然需要在脑中运行程序，但可以更分块地处理，无需理解包含千百个方法、类状态自动加载且到处被修改的复杂逻辑。此外还有REPL环境可随时尝试新代码。
在绝大多数情况下，你完全不必强迫自己编写命令式代码，状态变更操作通常也能在代码中实现局部化。当然，JavaScript和Python同样支持REPL环境。
但同样没人强制你写函数式代码。我看过海量的PHP和JS代码，其中大部分简直糟糕透顶哈哈。当然任何语言都能写出烂代码，但我认为JS/PHP入门门槛低且缺乏内置规范，容易让人堆砌出庞大的意大利面代码。
不过如今新建的TypeScript代码库通常相当规范。我钟爱TypeScript，能用这种类型化良好的现代项目开发，配合完善的模式验证等机制，体验实在太棒了。Clojure就缺这点。
另外我不太愿意把JS或Python的REPL和Clojure的相提并论。Python的REPL确实实用，但我几乎都泡在Clojure的REPL里。
我对CL接触不多只能推测，但严格的函数式编程原则通常能有效缓解动态类型的弊端。据我理解，CL在函数式编程方面并非最“纯粹”的实现，但它赋予程序员强大的系统约束与探索能力。
> 或许我们可以从更“笨拙”的语言入手，比如Rust或其他类型化语言。若追求代码正确性，动态语言绝非明智之选。类型检查才是最具价值且最常用的测试手段。
Lean或TLA+之于Rust/Java/Haskell的类型系统，正如代数拓扑与非线性偏微分方程之于“一个土豆，两个土豆”的简单概念。这类简单类型系统能实现的“正确性”程度，与丰富形式数学语言所能表达和证明的内容相比微不足道，几乎不值一提(它们确实能简化部分繁琐工作，但若讨论的是机器可处理复杂任务的世界，多些繁琐工作根本无关紧要)。
我的意思是…当然，但我只想要前80%的功能。而我们连这都没有。取而代之的是，我们用谁都搞不清具体功能的bash脚本构建内核和基础设施。我们需要一个坚实可靠的工具，让大型语言模型能够处理所有这些内容。
它应该具备熟悉的语法(比如C语言的命令式风格)，更易于阅读(或许带类型推断)，并拥有强大的现代类型系统(老天，给我总类型就够了)。或许是带(真实)类型的Python。
但若LLM已聪明到能处理编程的复杂部分，为何认为它们需要简单部分的帮助？反之，若它们不够聪明处理复杂部分，一点帮助又怎能带来显著改变？尽管努力探索，研究仍未能发现语言设计对人类程序员正确性或生产力存在显著的普遍性[1]影响(至少在中高阶语言中如此；我指的不是Java与汇编的对比)。我们各有偏好，且倾向于认为其具有普适性，但正是这种偏见使得实证研究不可或缺——而现有研究尚未得出定论。
如果对人类没有重大影响，为什么就假设对大型语言模型会有影响？我并非说大型语言模型像人类那样思考，但默认假设应该是：如果没有实例表明某件事会产生重大影响，那么它就不应该产生重大影响。换言之，若某事物未被证实具有影响，我们就不该假设它在此情境下会产生影响(当然可能存在，但需先找到可靠的实证依据)。
[1]：研究确实发现TypeScript与JavaScript存在特定差异，但该结论尚未得到普遍验证。
> 在我看来，在规范中使用panic是最懒惰且最糟糕的做法。
这正是为何“现有程序没有规范！”的哀叹完全为时过早。当今几乎所有代码库都存在作者认为不会发生的错误模式。
你只需开始证明这些情况不会发生。一旦着手证明，便开启了一段漫长旅程，最终至少能为程序的相当部分建立起正式规范。
证明panic是死代码的过程，本质上是你与证明助手/类型检查器之间的一种苏格拉底式对话，旨在厘清程序的现状与理想状态 :)。
或者直接使用返回Option<T>的API？若需异常处理，只需向上传递或手动抛出panic即可？
确实，Rust在形式化验证领域表现优异。霍尔规范契约(Hoare spec contracts)应是未来方向，尤其因其能自然延伸自单元测试。我用 Hax 效果不错。不过我怀疑，相较于通用模型，专用模型在精简证明求解方面的进步对程序验证的实际价值有限——尽管确实能大幅降低成本。
赞同。如今 AI 能解释一切，学习类型化语言变得容易多了。类型系统还能帮助 AI 编写正确代码，形成良性循环。
Rust转JS的转译器就很棒了。不知道是否有人像TypeScript那样把Rust做成前端语言。
这篇博文超出其专业范畴
– Lean将在底层用二进制大整数优化皮亚诺算术
– 属性检查与证明搜索本就存在连续性，反例本就是有效的(反)证明技术。战术编写者对此不应感到意外。
– 现有软件缺乏正式规范的问题，在这些技术普及后对绿地项目的影响将减弱。人们将更有动力明确需求，而成功实现需求将极大提升项目管理效率。
最后也是最关键的是，那些认为存在“宏大规格说明”与“宏大实现方案”的人完全偏离了本质。请记住，精益等工具本质上只是“更多类型”。当我们用类型编程时，难道会存在单一巨型类型与单一无类型项的配对吗？绝无可能。
高效软件开发的核心始终是不断积累更多库。更精妙的类型系统将催生处理各类任务“可复用核心”的创新库。
例如，你是否想编写能基于任意SQL模式实例化的“多态Web应用”？这类构想如今已可被清晰描述。
> 高效软件开发的关键在于不断增加库的数量
这句话让我无法认同。认为“更多库”能解决软件行业(相当严重的)质量问题，这种想法是…有失偏颇的。
参见：
https://www.folklore.org/Negative_2000_Lines_Of_Code.html
https://caseymuratori.com/blog_0031
除非真正需要，否则不要使用库。最近有人建议我在项目中添加Zod库，而整个项目中我仅需验证两个不同的JSON对象。我喜欢Zod，但已用原生JS逐步实现了类型验证功能。
少即是多，包括引入他人库时亦然。
Go谚语：
少量复制胜过大量依赖。
百分百赞同。这恰恰让AI辅助开发成为重大进步(只要谨慎使用)。你可以让大型语言模型为你编写小函数，或从庞大库中提取正确函数，直接内联到你的模块中。
赞同。
我指的是优秀语言中的卓越库。就像kmettverse彻底革新了Haskell编程方式那样——那些能让你重新审视目标的库。
多数人用的是垃圾语言里的垃圾库。NPM垃圾堆与我讨论的主题毫无关联。
> 优秀语言如[…]Haskell
我们对优秀语言的定义存在根本分歧
那我还真没想到你会认同我写的内容！
我的意思是，我认同优秀的类型系统是优秀语言的组成部分，但类型系统在整体中只占很小一部分。
Haskell的类型系统固然出色，却在我关心的诸多基础任务上惨遭滑铁卢：
[1] https://stackoverflow.com/questions/76470000/is-there-a-reas…
> 人们将被激励真正弄清楚自己想要什么
这才是我期待的通用人工智能。
> 人工智能辅助编程将编程边界从“可实现”拓展至“可定义”与“可验证”。
这点深有共鸣。当前我们编写代码的速度远超安全部署的速度。
> 当前我们编写代码的速度远超安全部署的速度。
这向来如此。从我们通过插拔跳线编程的年代起便是如此。
> 我们向来如此。从用跳线插板编程的年代起便是如此。
这对我来说是新知，而我可是开发界的古稀老者。
若团队配置为1名全职开发者配1名全职测试员，测试人员每天约有半数时间处于无所事事的状态。
当下，单凭一位掌握克劳德代码的开发者，就足以让数名测试人员应接不暇。
> 如今，单凭一位掌握克劳德代码的开发者，就足以让数名测试人员应接不暇。
因为AI编码产生的错误和问题永无止境且无法修复。测试人员以前会无事可做，是因为开发者在提交前会自行测试。但若让一群野蛮开发者每天编写数千行代码，完全不经测试就直接扔给测试人员，那么即便配备数千名测试人员，你也仍会抱怨人手不足。
> 因为AI编码产生的错误和问题永无止境，且永远无法修复。
但这正是我的观点 🙂
> 测试人员以前会无事可做，是因为开发者在提交前会自行测试。但若让一群粗放式程序员每天编写数千行代码，且完全不做测试就直接扔给测试人员，那么即使配备上千名测试人员，你仍会抱怨人手不足。
没错。但即便开发人员做了单元测试(这本是开发人员应尽之责)，他们仍可能让质量保证部门不堪重负。
我们以前从未能做到这一点。GGP声称我们始终可以做到。我反对的是这个具体说法——“我们总能让测试人员应接不暇”。
> 若团队配置为1名全职开发者配1名全职测试员，
你们居然有专职测试员！？我十四年开发生涯中，无论在FAANG巨头还是初创公司，从未见过这种配置。最接近的情况是某个约七个团队的时期，曾共享过两名测试员的服务。可想而知，这种比例下测试人员根本闲不下来。
我至少经历过4次这种情况；这是高度监管行业的工作副产品，该行业要求软件(或销售商品)必须符合特定认证标准(军工/军火/EMV等)。
在我曾任职的FAANG巨头和初创企业中，根本不存在质量保证部门，因此我推测这些公司也不设独立运作的质量保证部门。
不过这并非我的核心观点。关键在于我们永远无法比部署速度更快地输出代码。部署流程(含质量保证环节)始终快2到4倍。有时甚至快10倍。
=================
编辑：当然，我的从业年限约是你的两倍，当年大型企业设立专职QA部门相当普遍。就连微软也有这类部门呢 🙂
那是因为开发者得花三分之二时间修复测试人员发现的问题。
而编写新代码的时间，向来只是零头中的微不足道。
> 当前我们编写代码的速度远超安全部署的速度。
这种情况一直如此吗？
这篇博文中有许多值得商榷之处，但我想重点强调其中一点：形式化规范的必要性。这确实是个重大议题。然而必须区分两类规范：一类是足以证明功能正确性的完整规范，另一类则是针对特定安全或可靠性属性的规范，后者仅能用于验证这些属性。例如，我们可轻松定义“程序绝不读取未初始化内存”这一属性并完成验证。这虽不能保证程序功能正确性，但至少能排除整类潜在错误。
此处插一句题外话：我认同作者的核心观点，但拼写、语法错误和笔误反而让人感受到人类作者的存在。这句话：
“这影响到要点1，因为AI辅助编程与规范驱动开发天然契合。”
读来令人莞尔。这段未经现代网络写作过滤器和印刷机打磨的手工文字，恰似旧时手稿。
出乎意料的是，我最近竟在AI生成的代码里发现了错别字。不过这种情况确实罕见
训练数据里错别字比比皆是，提供RLHF反馈的人也常会忽略这些。
首先，他并非英语母语者。但我欣赏他没有用大型语言模型填补这个空白。
我认为当前更关键的是建立对抗性代理进行测试/验证——这在多智能体工作流中为我带来显著成效。当Claude首次推出“计算机使用”功能时，这在闭环流程中迈出了重要一步，避免了大型项目中繁琐的人工监管。需提醒的是这并非万能解，“分析器”仍可能出错，误判功能故障(或正常运行)，但它极大减少了“任务完成”的虚假报告——尤其当任务未完成或输出存在缺陷时。
所以它还不够可靠，无法自动运行？
我完全认同作者观点：AI辅助编程将瓶颈转移到了代码验证环节。
但其实无需完全形式化验证也能获得这些益处。测试驱动开发同样能实现多数目标。虽然验证结果可能不够绝对，但要达到高自动化测试覆盖率远比构建可形式化验证的代码库容易得多。
我认为AI辅助编程将引发对XP(极限编程)的重新关注，因为AI与XP两大核心理念高度契合：它能轻松生成经过充分测试的代码。而“结对编程”模式更是与AI助手协作的理想范式(远胜于氛围编程模式)。
问题在于TDD(测试驱动开发)与形式化证明在很大程度上都基于“复式记账”模型——即先编写测试/证明，再实现代码，最后确保两者一致。如同会计学假设，该方法认为人重复犯同样错误的概率较低，因此当两者一致时可高度信任准确性。当出现差异时，即可排查问题源于测试/证明还是实现。易犯错的人类极易在两者中出错。
但若仅填写账簿单侧(比喻而言)，大型语言模型会欣然编造出确保账目平衡的内容——即便你填写的记录完全错误。因此，这种开发方式虽优于盲目信任任意提示而缺乏制衡机制，却未能真正实现与以往同等程度的代码验证。这仍是未解难题。
我不太理解你所说的“会计学认为重复犯同样错误的概率很低”？复式记账法只能判断账目是否平衡，绝不能因此就认定账面反映了真实情况。账面要失真，根本不需要重复犯错。
此外测试与代码是独立的，而复式记账必然同时影响两侧。审计制度的存在自有其道理。
在复式记账中，错误唯一可能漏检的情况是双方都犯同样的错误——否则账目本就无法平衡。测试同样如此：若测试和实现都存在错误，它们可能相互抵消，表面上看似无误。
然而我并不完全认同这种推理，因为测试未能检验应测试的属性，与该属性实现中的错误属于截然不同的错误类型。错误无需在两端都出现“相同”的错误才会被忽略。相较于簿记，测试或实现中单个随机错误更可能不被察觉。
> 在复式记账法中，错误唯一可能漏检的情况是记账两侧出现相同错误——否则账目必然失衡。测试领域同样如此：若测试与实现两端均存在错误，它们可能相互抵消，从而看似无误。
没错，但测试与代码的性质截然不同，对吧？每笔账目至少有两个方面，且需同步处理，不像测试和代码那样相互独立。
若记错账目仍能保持账面平衡，这恰恰说明问题所在——账面平衡≠账目准确。在复式记账法中，“代码”与“测试”并无区别，本质上都是“代码”。
看来提出这个比喻的人要么根本不懂复式记账原理，要么只上过一门会计课。
> 是啊，但这和测试与代码的关系完全不同，对吧？每笔分录至少有两个方面，需要同步处理，不像测试和代码那样独立。
当前讨论的核心在于：人工智能编码代理的运用可能破坏这种平衡。例如它们可能观察到真实阳性测试失败后，选择修改测试以确保通过。
“高置信度”这个概念哪里难以理解？
请收敛些刻薄语气。“高置信度”本身不难理解，但你的比喻毫无意义。账目平衡≠账目准确，这绝非记账精确的标志。这些条目也并非像代码和测试那样相互独立。
> 账目平衡≠账目准确
理所当然。正因如此才用“高度可信”而非“完全可信”。但别在这点上纠缠过深。回归正题，“高度可信”这个概念具体哪里难以理解？
理论上说得通，但实践中采用TDD时我的代码质量远高于不采用时。无论是否使用AI编码助手，这个结论都成立。
我认为GP并非持反对意见。他们(我理解)是指出AI辅助的TDD不如人工TDD可靠，因为AI会为了通过测试而编造毫无意义的测试用例。
两者存在根本差异：TDD旨在规避前期设计，而形式化规范本身就是前期设计。
过去二十年主流实践正逐步接纳XP理念——先是DevOps，如今又引入智能代理辅助的结对编程与TDD。
上周相关讨论：
人工智能将推动形式化验证主流化
https://news.ycombinator.com/item?id=46294574
关于人工智能与软件形式化验证的讨论令我困惑不已。这好比有人说：假设我能弄来起重机把那辆古董车吊进15楼公寓的客厅，那我的行李箱该怎么办？
文章提及的所有问题都很严峻。但比起让AI自动验证数十万甚至数百万行程序中至少数百个正确性属性，这些问题都简单得多。引入高等数学讨论也毫无助益——有趣的数学定理证明需要独创性与创造力，而软件正确性验证则不需要，且前者所需的引理和推理步骤数量级更少。我们讨论的是每行程序代码对应100至1000行的证明工作量。
虽不知人工智能何时能实现这一切，但我认为具备此能力的计算机，理应能将正确性属性的形式化表述与非正式需求相协调，甚至将需求本身与市场需求精准匹配。
我想表达的是，一台能够可靠地编写复杂大型软件并证明其正确性的机器——顺便说一句，人类目前尚不具备这种能力——很可能也能根据提示完成任务：编写一款在35-65岁女性群体中广受欢迎的软件，更不用说“编写一个功能强大如Excel但更易用的电子表格”了。当然，一旦这种情况发生，任何此类软件的市场价值都将归零，因为任何人都能给出这样的指令。事实上，我们所知的软件将失去存在意义，因为人工智能完全可以直接实现软件应有的功能(尽管它可能选择生成可执行文件作为实现细节)。
我看到的是人们耗费大量时间想象如何与能解决重大问题却又无法处理简单任务的人工智能协作，实在不明白这种设想有何意义。
致验证专家：(恕我数学理解近乎为零)
> 这使得形式验证成为人工智能辅助编程的首要目标。既然我们拥有形式化规范，只需让机器持续探索数小时、数日甚至数周。
这种观点是否完全忽略了：满足特定要求的程序可能存在多种实现方式，且均能输出正确结果？其中许多方案在性能、时间复杂度等方面岂非糟糕透顶？我明白在最简单的案例中，AI不会直接跳到O(n³)级别的解决方案，但同样无法保证其不会产生损害性能的缺陷——只要这些缺陷不影响技术正确性。
另外，难道我们还假装让Claude持续运行“数周”是免费的？
经过验证的软件必须满足活性属性；否则，一个永远不会返回的无限循环也能被判定为“正确”。
实时软件的验证要求更为严格，必须确保算法在所有情况下完成所需的最大时钟周期数存在上限。
没错，我用Claude验证代码已经花了2万美元左右，所以成本确实有压缩空间。
我虽不及作者学识渊博、文采斐然，但有相近见解：规格定义既困难又耗时，而漏洞从不关心自己是否属于官方规范。
部分软件需要形式化验证，但所有软件都需要测试。
另提一事…
> 测试虽擅长发现缺陷…却无法证明缺陷不存在。
但愿更多人能理解这点。
除非人们因此认定测试毫无必要…这种情况在学术界屡见不鲜。这也是某些大学测试教学不力的原因之一…
这难道不会陷入与开发人工智能优先语言相同的瓶颈？人工智能需要海量训练数据来学习如何编写优质的正式验证代码，或编写尚不存在的新型人工智能优先语言代码。唯一解决方案是大规模合成生成，但若人类在某种程度上无法验证合成数据的有效性，这项工作将难以推进。
我认为该文章在以下几个方面仍低估了形式化规范的价值：
– 形式化规范可用于推导随机生成的测试用例，以寻找规范不变式的反例(文章虽有暗示但未明确说明)
– 形式化规范可作为模型检查器的输入，通过对模型状态空间的有限探索来寻找规范不变式的反例
– 可通过分析生产系统的运行轨迹，利用形式化规范发现规范不变式的违反情况
这些案例的共同点在于：它们试图证伪而非验证规范是否准确描述了预期设计属性或实际实现。相较于真正证明规范正确性，这种方法往往更具可行性。
> 这种方法还极其耗时——在CPU中本应瞬间完成的a+b运算，其计算复杂度竟达O(a+b)，因为加法操作的时间复杂度随数值大小呈线性增长，而非常数级。
对我而言，这构成了应用领域的难以逾越的高墙。我们讨论的是验证由AI快速生成的系统。若验证步骤慢如蜗牛(无论如何衡量，百万周期完成两个整数相加都算极慢)，我实在看不出这如何能成为可行的解决方案。
人们连写代码都懒得动，你还指望他们去测试？
我好奇基于契约的设计或模式优先设计是否能成为一种新趋势，用于结构化AI输出并使其快速迭代达成目标。我正尝试将这些方法应用于AI实践，探索其发展方向。正在研究https://deal.readthedocs.io/
形式化验证虽是好主意，但从当前阶段看仍是座大山。多数人连让智能体可靠地进行端到端代码质量检测都做不到——这座山虽然低得多，却可能带来更大收益。不过我确信该领域终将进步，毕竟这是实现完全自主工程的终极突破口。
我认为对多数复杂系统而言，全面的端到端质量保证实属浪费。少量端到端烟雾测试配合精心设计的局部测试通常已足够。不过公平地说，智能代理在这方面同样表现欠佳。
我认为《从零到QED的人工智能》(精益/语言指南中的证明)中关于人工智能的章节，从做市商和交易视角提供了清醒的进路：
"设想这样的市场基础设施：代理在执行前必须证明其行为满足监管约束、风险限额、公平属性，并最终提供可机器验证的市场机制帕累托效率证明。这是个宏大而复杂的雄心勃勃的目标。不是’我们审查了代码’，而是’系统验证了证明’。无法证明合规性的代理将被禁止行动。"
https://sdiehl.github.io/zero-to-qed/20_artificial_intellige…
我梦想着这样的未来：在任何软件发布前，我们能预测其百年后的影响，若某物种的不幸增量低于阈值，便禁止发布。
这需要将生物行为纳入形式化规范，实则不可行。
> 传统证明助手并不使用我们内存中按字节打包的经典二进制补码整数，而是采用皮亚诺数
为何不能直接用标准二进制补码整数证明定理，而非使用自然数？
当然可以。自然数成为默认选择，是因为编写和使用证明助手的人群通常优先采用自然数思维，而非编程中使用的模2^N的2进制数，甚至比算法中使用的普通2进制数更优先。这就像数学家偏爱1基索引一样——虽然违背编程惯例，但使用者更觉得顺手。
我闻到了 vaporware 的味道。形式验证对简单函数这类基础内容容易实现——复杂函数可能根本无法验证。届时你大概率会遇到一群兜售灵丹妙药的推销员，承诺能验证完整系统…
你所说的复杂函数具体指什么？为何认为其性质无法验证？
测试即可，无需验证。
我如何学会更快部署。
> 人工智能正推动形式化验证走向主流。
又是这种无稽之谈。不，绝非如此。
销售者当然希望如此，但这并不代表事实。
你根本没关注过。
我们今天在此讨论它，过去几周也持续关注它——这本身就是证据。更关键的是，在去年十一月之前，我们根本没听说过这些。Opus 4.5和GPT 5.2已跨越实用性边界。
据我观察，过去一个月我通过编写Alloy模型并确保代码兼容性，在引导大型语言模型方面取得了一定成效。若放在今年夏天，从投资回报率角度看，这些尝试根本不值得尝试。技术格局已发生质变。
> 我们今天在此阅读相关报道，且过去数周持续关注此事，这本身就是证据之一。另一证据是：在去年十一月之前，我们根本没见过相关报道。
不过我记得过去几年里，这里确实多次出现过相关讨论。
形式化验证正成为茶水间闲聊的热门话题。作为深耕函数式编程和依赖类型领域十余年的从业者，我认为这是巨大的进步。
从业余项目到日常工作的方法论管道已然成型。
据我所知，LLM式AI并不擅长形式化验证。而近期AI领域的突破，对真正适用于形式化验证的AI类型帮助甚微。
形式验证并非直接由AI执行。而是让智能体访问验证工具，其输出结果再反馈至模型。
这与向LLM提供当前时间的设计原理相同——毕竟它们同样无法自行识别时间。
我们短期内不会正式验证数百万行代码，别抱太大期望。
…但我们会对跨多个服务、处理关键业务逻辑或分布式事务的5-10千行代码模块进行建模。这在几个月前还难以想象，如今只需一次“只读星期五”实验就能实现(用前沿模型试试看，你会惊讶)。
Alperen，
感谢这篇文章。或许你能撰写一篇关于你推崇的“验证引导开发”方法的后续文章或教程？这对包括我在内的大多数人都是新概念，而你在文中主要探讨了不喜欢的内容后，仅对其进行了简要提及。
祝你顺利完成学位！
附注：您研究页面的部分链接是占位符或已失效。
我会补充原始VGD论文及相关文章的链接，短期内应该能解决问题。感谢提醒！未来几周我会着手撰写关于VGD本身的专题内容。
真是篇精彩的读物
归根结底，要么手动验证每行代码，要么让智能体编写测试。实现代码审查自动化。
另见Regehr案例[1]：某形式化验证C编译器因<limits.h>中值不一致产生错误输出(简而言之：编译器可选择“char”的符号/无符号属性。Compcert选定一种，但Linux系统头文件在CHAR_MIN和CHAR_MAX中使用了另一种)。
1: https://blog.regehr.org/archives/482此处存在诸多问题，不仅限于Compcert
我用户应该为此获得赞同票 🙂
哈哈，这-3分值了