1979 年一篇论文挑战了程序验证这一新兴领域，作者为 Richard DeMillo、Richard Lipton 和 Alan Perlis。

• 背景：程序验证始于 20 世纪 60 年代末，如 Robert W Floyd 和 Tony Hoare 的相关工作，早期验证工具能力有限且缺乏可靠逻辑基础，1979 年作者抱怨缺乏对工作系统的验证。
• 他们的论点：基于两个支柱，一是形式证明极低级、冗长不可行，以 Whitehead 和 Russell 的《数学原理》为例；二是数学家通过讨论验证证明的传统方法是确立任何命题真实性的正确方式。
• 从 21 世纪看他们的论点：其论点未经受住时间考验，之后很多重要数学结果用证明辅助工具从“第一原则”证明，大量数学已被形式化，如 Ramanujan 的一个定理。关于第二支柱，虽有数学论文中错误被纠正的例子，但数学家对错误的态度已改变，如 Isaac Newton 研究所举办相关研讨会。
• 验证计算机系统：真实程序可能很长且规格复杂，虽难以验证整个 Microsoft Word，但已有如 seL4 操作系统内核等被验证，硬件验证更成功，如今验证技术已嵌入公司开发过程。
• 目的何在：难以理解作者写作的动机，当时虽有一些程序验证工作，但远未普及，他们似乎在反对一个并不存在的“恶龙”。
• 他们正确的地方：指出从非正式需求到正式程序的过渡必须是非正式的，强调好证明应让人更明智，注重直觉在理解数学概念中的作用，以及批评一些所谓的“验证”只是形式证明而难以让人理解。
• 尾声：感谢作者找到 Jech 书中列出错误的那一页，作者对数学错误的态度让作者想起反疫苗者，应重视并改进数学验证等工作。