math - 为什么程序不能被证明？

Question

为什么计算机程序不能像数学陈述那样被证明？数学证明是建立在其他证明的基础上的，而其他证明又是由更多的证明和公理建立起来的——我们认为这些真理是不言而喻的。

计算机程序似乎没有这样的结构。如果你编写一个计算机程序，你如何能够采用以前经过验证的作品并用它们来证明你的程序的真实性？你不能，因为不存在。此外，编程的公理是什么？该领域的原子真理？

对于上述问题我没有很好的答案。但软件似乎无法被证明，因为它是艺术而不是科学。如何证明毕加索的作品？

Answer 1

证明 are程序。

Formal verification程序是一个巨大的研究领域。 (例如，参见the group at Carnegie Mellon。)

许多复杂的程序已经被验证；例如，请参阅此 kernel written in Haskell (修复的 404 链接适用于 seL4 ，另请参阅 moved to location 和 project's website )。