鲍勃叔叔是认真的吗？

罗伯特·C·马丁（人称“鲍勃叔叔”）多年来一直不遗余力地强调“软件专业精神”，我对此深表赞同。我认为，作为专业人士，软件开发人员确实需要大幅提升自身水平。然而，我对鲍勃叔叔的做法开始感到担忧。前几天，当我读到他那篇题为《工具并非答案》的博文时，我彻底崩溃了。

他反对《大西洋月刊》最近的一篇文章：《即将到来的软件末日》。让我试着概括一下这两篇文章的论点。

《大西洋月刊》：

我们正在为安全关键型应用编写越来越多的软件，这些软件变得如此复杂，以至于程序员无法穷尽地测试或理解软件可能遇到的所有输入、状态和交互。我们试图构建的系统已经超出了我们自身的认知能力。

面对如此复杂的环境，我们需要新的方法来帮助软件开发人员编写出功能正确（且安全）的软件。目前开发安全关键型软件的方法对社会尤其危险，因为当软件存在缺陷时，我们无法像观察轮胎是否漏气那样观察到它们——它们是隐形的。

鲍勃叔叔：

原因：

1. 太多程序员在时间压力下偷工减料，走捷径。
2. 太多其他程序员认为这样做没问题，并为之掩盖。

显而易见的解决方法是：

1. 提高软件开发规范性和专业水平。
2. 永远不要为工作马虎找借口。

鲍勃叔叔的论点经得起推敲吗？

《大西洋月刊》文章探讨的安全关键型软件系统，其质量标准之高令人震惊。这些系统所涉及的需求分析、规划、设计、编码、测试、文档编写、验证以及合规性等工作，远远超出普通企业开发电商网站或移动应用时的标准。

读读《他们写对了东西》（They Write the Right Stuff）这篇文章，告诉我你觉得鲍勃大叔的观点是否正确（请注意，这篇文章写于21年前，如今的技术已经取得了长足的进步）。你觉得NASA的程序员们是不是只需要加强纪律和专业精神，并且永远不要为工作马虎找借口？

一位来自麻省理工学院的安全关键系统专家有什么看法？

《大西洋月刊》的文章多次引用了南希·莱维森博士的话，但鲍勃叔叔完全忽略了这些内容。

让我们来回顾一下她一次演讲中的一段摘录：

我从事这行三十六年了。我读过数百份事故报告，其中很多都涉及软件。而所有与软件相关的事故，都是需求问题，而不是代码问题。所以，这是第一个真正重要的问题。大家都在忙着编写代码和测试，却忽略了需求，这才是问题的症结所在。（重点为笔者所加）

她已经说得很清楚了。我有没有说过她是专家？我有没有说过她参与过各种重要项目，包括政府机密武器项目？

约翰·C·奈特博士怎么样？

在题为《安全关键系统：挑战与方向》的论文中，奈特博士描述了构建安全关键系统所面临的诸多挑战，但开发人员的纪律性和专业精神却不在其中。这大概是他在这方面所能达到的最接近的程度了：

现有技术下，安全关键型系统的开发时间和精力投入极其巨大，以至于在很多情况下，构建未来所需的系统将变得不可能。该领域的任何新软件技术都必须同时解决成本和时间问题。这项挑战十分艰巨，因为降低几个百分点的影响微乎其微，需要实现数量级的提升。

开发安全关键型系统极其缓慢，这会增加成本。但质量保证实践几乎可以确保交付的软件功能完全符合需求。鲍勃大叔可能会辩称，有些项目进展缓慢是因为这些项目的开发人员缺乏纪律和专业精神。但这种说法需要证据，而鲍勃大叔拿不出任何证据。

是的，工具是解决方案的一部分（但不是全部解决方案）。

我的天哪，我们需要更多更好的工具。我刚开始学编程的时候，用的只是一个带基本语法高亮功能的文本编辑器，仅此而已。我以前都是通过 FTP 上传代码到生产服务器运行，根本没有开发环境。

更好的工具帮助我成为了更优秀的程序员。

后来我改用了Eclipse，觉得之前没早点用真是太傻了。Eclipse能发现我用普通文本编辑器漏掉的各种错误。它就像文字处理器里识别拼写错误一样，直接把它们高亮显示出来——简直太棒了。

几年后，我采用了 Subversion 作为我的版本控制系统，我当时就觉得自己没早点用上真是太傻了。我可以查看项目的全部历史记录，可以进行修改，也可以撤销修改。简直太棒了。

同上：

• 代码审查/拉取请求/Jira
• 高级集成开发环境 (IDE) 集成了静态分析、自动重构工具、自动代码格式化和一键运行的单元测试。
• GIT/bitbucket/GitHub
• 测试驱动开发
• 基于属性的测试（QuickCheck系列）
• 虚拟机
• 框架
• 开源库

我开始编程已经快二十年了，这些年来我的工具发生了翻天覆地的变化。我简直无法想象未来二十年里涌现出的新工具会如何改变我们编写和交付代码的方式。

我们来看看几种可能性。

更好的静态分析器

我的静态分析器仍然无法理解我的代码，只能检测到一些简单的错误。它们会发出大量的误报。在大代码库上，它们的速度也很慢。我真希望只有一个静态分析器就能满足我的所有需求，而不是现在用的四五个。编写自定义规则也很耗时。这方面还有很大的改进空间。

通过施工技术进行校正

还有一些“构造正确”的技术。我看过这个视频，他提出的“可证明不存在运行时错误”这一点就让我很感兴趣。于是我找了一本关于Spark（Ada 的一个子集）的书开始学习。哇，你或许可以用 Spark 写出高度可靠且正确的软件，但这将是一个缓慢的过程（也就是成本很高）。

这就是未来吗？我不知道，但如果 Spark 的编程更容易上手，它在安全关键型软件领域或许会有更大的发展前景。如果有人能为我最喜欢的编程语言开发出既精确又易用的形式化方法功能，那就太好了。“无需为这个模块编写测试，证明器已经证明它在数学上是合理的”，这简直太棒了。

2020年10月23日更新：
我最近用Ada/SPARK编写了一个相扑机器人程序，以便更好地了解这两种语言。我认为你会对Ada/SPARK要么爱不释手，要么嗤之以鼻。如果你喜欢Python的速度和灵活性，你很可能会讨厌Ada/SPARK。但如果你注重低缺陷率和高质量，你一定会喜欢Ada/SPARK的那些特性，它们能帮助你实现这些目标。

该软件用于跟踪每个需求，从实现该需求的代码到证明代码已正确实现的测试。

我观看了一段视频，视频中一位主讲人谈到她的团队在安全关键型系统中，为了满足监管合规要求，需要追踪成千上万条需求与特定代码和测试用例之间的对应关系，这给他们带来了很大的困难。随着项目推进，需求、测试和代码不断变化，他们努力保持所有内容同步，这项任务变得更加艰巨。像他们这样的团队以及所有类似的团队都需要更好的工具。最终，如果易于使用，我非常希望看到我最喜欢的编程语言的集成开发环境（IDE）能够内置类似的功能。

形式化规范语言/模型检查器

接下来，我们还可以考虑形式化规范语言。《大西洋月刊》的文章提到了 TLA+，但还有其他语言。现在想象一下，如果这些语言都很容易使用呢？想象一下，你有一个工具可以帮助你以迭代的方式构建形式化规范，它会引导你一步步完成，确保你涵盖所有情况。完成后，它还可以为你生成部分或全部代码。此外，如果你遇到问题，可以直接在 Stack Overflow 上找到答案。酷吧？当然酷！

还有更多……

我相信我们可以在评论中集思广益，提出几十种新的或改进的工具，帮助我们以更低的成本编写更好、更正确的代码。

为什么加强纪律和专业精神并非解决之道

根本问题在于，即使是我们中最聪明的人，也没有足够的智力去理解和推理我们试图构建的复杂交互系统中可能发生的所有事情。这并非学科或专业水平的问题。这些系统可能会表现出涌现行为，或者运行正常，但其运行方式却是设计者无法预见的。

这就是莱维森博士的书如此重要的原因。我们不必费尽心思去弄清楚所有状态和行为，而只需明确指出哪些状态和行为是不安全的，并阻止软件进入这些状态即可。当然，实际情况要复杂得多，但这只是其中的一部分。

结论

我完全赞成提高软件开发的专业性和规范性，但鲍勃大叔对于如何防止安全关键型软件系统中的“软件末日”的说法是错误的。业内专家并没有把程序员的专业性和规范性列为防止损失的首要任务之一。

提高程序员的纪律性和专业性固然有益，但我们也需要控制复杂性的方法、更好的工具、提高生产力的方法、对涌现行为进行推理的方法、研究哪些方法对开发安全关键型软件系统真正有效、针对软件开发过程各个方面开发新的更好的技术，特别是更好地获取正确需求的方法，等等。

我知道有很多程序员在编写低质量代码。但是，构建安全关键系统的组织都有相应的流程来防止绝大多数此类代码进入他们的系统。所以，如果软件末日真的来临，你可以相当肯定这不会是因为某个程序员想走捷径蒙混过关。

你觉得呢？同意还是不同意？我很想听听你的想法。

更多资源

博客文章：安全关键型软件：每位开发人员都应该了解的 15 件事

这是鲍勃大叔关于软件行业职业素养的演讲视频：https://youtu.be/BSaAMQVq01E

南希·莱维森的著作《构建更安全的世界》非常重要，她已将其全文免费发布：https://www.dropbox.com/s/dwl3782mc6fcjih/8179.pdf? dl=0

关于安全关键系统的精彩视频：https://youtu.be/E0igfLcilSk

关于“构造校正”技术的精彩视频：https://youtu.be/03mUs5NlT6U