proof - 有没有办法证明程序没有错误？

Question

我在想这样一个事实，即我们可以证明一个程序有错误。我们可以对其进行测试以评估它或多或少具有抗错误性。

但是有没有办法(甚至理论上)证明程序没有错误？

对于简单的程序，例如“Hello World”，我想我们应该可以做到。
但是更大的程序呢？

Answer 1

现在有许多不同的形式可以用来证明程序的正确性(例如，证明助手中的形式化，依赖类型的编程语言，分离逻辑，......)。正如其他人所指出的，没有自动的方法来证明任何给定的程序是正确的(参见停机问题)。然而，那些提到的形式主义通常适用于特定的程序。 (这样的应用程序可能远非自动化，需要大量的创造力。)

另一个非常重要的一点是我们通过证明程序正确或如您所说证明程序没有错误的实际含义。即使使用正式方法，通常也无法说 什么都没有程序可能会出错。原因是形式方法通常表明程序符合规范。

您可以将规范视为逻辑公式(说明程序的某些属性)，将正确性证明视为程序满足此公式(即，具有相应的属性)的形式证明。由于这种设置，规范之外的所有内容都不会被证明“考虑”。因此，要真正证明程序没有错误，您首先必须写下一个逻辑公式，说明程序何时没有错误。

所以说正式方法通常能够证明(毫无疑问)一个程序没有某些类型的错误(取决于所使用的规范)可能会更诚实。