Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia
本文通过对 30 位业界和学术界从业者的访谈进行了一项定性研究，旨在识别阻碍演绎验证广泛采用的已知及尚未被充分探索的障碍，并最终为从业者、工具构建者和研究人员提供具体的建议，以提升可用性、自动化程度以及工作流集成度。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下你正在建造一座摩天大楼。你希望百分之百确定它不会坍塌，电梯永远不会卡住，且火警系统始终有效。你可以雇佣一个检查小组在建筑建成后进行检查（这类似于标准测试）。或者，你也可以雇佣一个数学家团队，在第一块砖铺下之前，就利用纯逻辑来证明这座建筑不可能发生故障。这种数学证明被称为演绎验证（deductive verification）。
这篇论文是一份研究报告，研究人员走访了 30 位专家——那些真正从事为软件编写此类“数学证明”工作的人——了解这份工作的真实体验。他们想知道：为什么不是每个人都在做这件事？什么让它运作良好，又是什么让它变成一场噩梦？
以下是他们的发现，用通俗易懂的语言进行了说明。
大局观：为什么不是每个人都在做这件事？
尽管演绎验证功能极其强大（它就像是拥有你的软件绝无漏洞的保证），但它并未被广泛应用。它主要用于非常关键的任务，例如运行核电站或安全军事系统的软件。对于普通的视频游戏或购物应用，它通常被认为成本过高且难度太大。
研究人员发现，虽然我们已知其中一些问题（比如“学习难度大”），但他们发现了许多新的、令人惊讶的难题，而这些问题却鲜有人提及。
好消息：什么时候它确实奏效？
专家们表示，如果你遵循以下黄金法则，验证就会大获成功：
- 选择战场： 不要试图证明整座摩天大楼都是完美的。只需证明地基和消防逃生通道是完美的即可。将精力集中在软件中最关键、最危险的部分。
- 尽早开始： 如果你等到建筑完工后再开始进行数学证明，那你麻烦就大了。你需要从第一天起就在设计建筑时就考虑到证明的需求。
- 工具需要友好： 想象一下，如果你试图用一把重达 50 磅且没有手柄的锤子来盖房子，那会是什么感觉。专家们说，验证工具需要变得更容易使用，就像一把带有良好握感的电动钻头。
- 融入工作流： 你不能要求施工队停止使用蓝图，转而开始在餐巾纸上画图。验证需要融入开发者现有的工作方式，而不是强迫他们改变整个生活方式。
坏消息：隐藏的头痛问题
论文揭示了几个让验证变得困难的“底层”问题：
- “移动目标”问题（证明维护）： 这是一个巨大的惊喜。想象一下，你证明了你的桥梁是安全的。然后，你决定给桥涂上不同的颜色。突然间，你的数学证明失效了，你不得不重新做一遍整个过程。在软件中，代码一直在变化。使数学证明与不断变化的的代码保持同步是一项巨大且令人精疲力竭的苦差事。目前还没有好的工具能帮助你在代码变化时修复证明。
- “黑盒”问题（自动化）： 自动化是一把双刃剑。一方面，它为你完成了复杂的数学计算（这是一件好事）；另一方面，当它失败时，它只会显示“错误”，而不告诉你为什么（这是一件坏事）。这就像一辆车无法启动，仪表盘只闪烁红灯却没有任何解释。开发者觉得自己在与一台看不见内部构造的机器作斗争。
- “翻译器”问题（编写规范）： 在你证明任何事情之前，你必须用一种极其严格的数学语言准确地写下软件应该做什么。这非常困难。这就像试图向一个没有常识的机器人解释一道复杂的食谱。如果你遗漏了一个微小的细节，整个证明就会失败。
- 思维转变： 普通程序员思考的是“这是否可行？”而验证专家思考的是“这是否可能失败？”这需要完全不同的思维方式，这很难学习，甚至更难教授。
建议：我们如何解决？
基于这些访谈，研究人员向三个群体提出了建议：
给管理者（老板们）：
- 不要试图验证所有内容。只验证那些最重要的部分。
- 在项目初期就开始考虑验证，而不是将其作为事后的补救措施。
- 投资于团队培训；这是一项很难掌握的技能。
给工具开发者（开发者）：
- 消除黑盒： 让工具透明化。如果数学计算失败了，请展示给用户看为什么。让他们看到内部齿轮是如何运转的。
- 协助维护： 开发能够当代码发生轻微变化时，自动更新数学证明的工具。
- 提高可用性： 增加诸如自动补全和更好的错误提示等功能，就像现代编程工具那样。
给教师（研究人员与教育工作者）：
- 不要只教理论。要教学生如何在实际项目中利用真正的工具。
- 创建一个“模式库”，这样学生在尝试证明某些内容时，就不必每次都从头开始造轮子。
总结
演绎验证是一种超能力，但目前来看，它是一种需要大量培训、昂贵工具以及大量耐心来应对变化的超能力。论文认为，如果我们希望这项技术走向主流，我们就不应仅仅关注如何让数学变得更“聪明”，而应开始关注如何让工具更人性化、更易于维护，并更好地解释出错的原因。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。