问题描述
为什么不能像数学语句一样证明计算机程序?数学证明是建立在其他证明之上的，而其他证明则是从更多的证明到公理(我们认为是不言而喻的真理)的基础上建立的.
Why can't a computer program be proven just as a mathematical statement can? A mathematical proof is built up on other proofs, which are built up from yet more proofs and on down to axioms - those truths truths we hold as self evident.
计算机程序似乎没有这样的结构.如果您编写计算机程序，那么如何才能接受以前已被证明有效的作品并使用它们来展示程序的真实性?您不能，因为不存在.此外，编程的公理是什么?该领域的原子性真相?
Computer programs don't seem to have such a structure. If you write a computer program, how is it that you can take previous proven works and use them to show the truth of your program? You can't since none exist. Further, what are the axioms of programming? The very atomic truths of the field?
我对上述内容没有好的答案.但是似乎软件无法证明，因为它是艺术而不是科学.您如何证明毕加索?
I don't have good answers to the above. But it seems software can't be proven because it is art and not science. How do you prove a Picasso?
推荐答案
证明是程序.
程序的正式验证是一个很大的研究领域. (例如，参见卡内基梅隆大学的小组.)
Formal verification of programs is a huge research area. (See, for example, the group at Carnegie Mellon.)
许多复杂的程序已经过验证；例如，请参见用Haskell编写的内核.
Many complex programs have been verified; for example, see this kernel written in Haskell.
这篇关于为什么不能证明程序?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！