软件工程为什么需要形式化方法？ - ntietz

软件工程师的工作不是编写代码，而是解决问题；我们碰巧通过生成代码解决了大部分问题。最终，生成代码很困难，我们需要帮助。这就是为什么 GitHub 的Copilot令人兴奋，但它远非理想，它只是已经完成和将要发生的事情的冰山一角。

Copilot 上有很多热门话题，所以我不会非常深入地探讨这次特定发布的缺陷（道德问题、引入错误等）。归根结底，这是非常令人兴奋的，并且像所有基于统计推理的工具一样存在缺陷。（这是一个非常重要的领域，人们在围绕机器学习的 HCI 和 UX 方面有很大的进步空间。）这很有帮助，因为它可以减少生成代码的摩擦，这是必要但最终的一小部分软件工程师的工作。它只是我们编码时所做的一部分！

通常的编码过程（对我来说）看起来像这样：

• 指定：弄清楚代码需要做什么
• 实施：编写有问题的代码
• 验证：测试代码以确保它执行所需的操作
• 迭代：根据需要冲洗并重复多次（增量开发、修复错误等）

这里跳过了提前收集需求所需的所有工作；这只是编码部分。

所以 Copilot 和我见过的其他代码生成工具处理实现位：他们编写有问题的代码，不尝试或保证正确性或完整性。这是一个起点，这很棒。但是，它确实强调了我们需要多少关注规范和验证步骤。如果我们有简单的代码生成可用，那么作为一个人在压力下快速发布代码只是说“对我来说看起来不错”并发布它是非常容易的。这就是你如何获得微妙的错误和遗漏，从长远来看，这只是编程，而错过了整个工程部分。

如果我们可以为某段代码编写规范，然后让机器完成其余的工作，那岂不是很棒？我知道，我知道，人们已经尝试了很长时间，但它令人担忧。我并不是说我们可以在今天或十年后在理论上或实践上做到这一点。但作为一个目标，那真的是你想要的东西：我们想要说给解决问题“这是解决方案”，然后噗的出现解决方案！对某些人来说，副驾驶感觉就像是魔法一样，这很危险。它跳过了验证步骤，我认为它也跳过了指定您想要的内容（因为文档字符串通常不是很清楚、模棱两可，并且错过了非常重要的非功能组件，如性能和安全性）。

那么，这会把我们带到哪里？嗯，我们想做工程来解决问题。我认为这意味着，实际上，我们需要专注于规范和验证步骤，并确定更好的方法，同时努力改进实现工具（更好的自动完成、代码生成等）。

如果我们可以改进规范和验证步骤，我们将从有缺陷的实施工具和技术中获得更多的收益，并且无论如何我们都能够在实施步骤上更快地移动，因为我们知道我们可以快速移动并犯错，因为他们会被抓住。良好的规范和验证可以加快实现部分的速度，同时为您提供更好的结果。

软件工程的未来倾向于形式化方法，并依靠形式化方法为我们提供更高质量的输出。

未来就在这里，有点！您可以使用一些工具来更严格地指定和验证您的代码和系统：

• TLA+ 是房间里的大象，已被大量用于验证AWS和 MS 等系统；可能是一个很好的起点！
• 属性测试（比如Python 的假设）也是一种形式化方法，它可以带你走很远，如果你已经有了单元测试，那么它是轻而易举的成果。它可以让您获得更高级别的保证，而不必完全形式地验证您的程序。
• 甚至静态类型也是形式方法的一种形式，即使在 Python 和 Ruby 等语言中也越来越多地接受它们！将来，我们可以通过细化类型进一步改进，以获得围绕值的良好的强大编译时保证。
• 还有很多我不知道的，因为我是这个领域的新手。（给我发电子邮件或推特给我推荐！）

这并不是说所有的代码都需要或受益于形式化方法；一些一次性脚本或简单的 Web 应用程序可以在没有它的情况下制作，并且使用形式方法会太昂贵。这很好，这表明我们的领域存在分歧：软件工程与软件开发。随着我们找到谈论软件工程的工程方面的方法以及指定和验证我们的程序的更好方法，随着时间的推移，这种分歧可能会变得更加清晰。

我个人倾向于这个。我倾向于从事正确性、稳定性、可靠性和安全性都非常重要的事情，因此形式化方法提供了一种改进这项工作并实现这些价值的方法。我的学习清单上的第一个是 TLA+。