Por que um programa de computador não pode ser provado da mesma maneira que uma afirmação matemática? Uma prova matemática é construída sobre outras provas, que são construídas a partir de mais provas e até axiomas - essas verdades, verdades que consideramos evidentes.

Os programas de computador não parecem ter essa estrutura. Se você escreve um programa de computador, como pode executar trabalhos comprovados anteriores e usá-los para mostrar a verdade do seu programa? Você não pode, pois não existe. Além disso, quais são os axiomas da programação? As verdades muito atômicas do campo?

Não tenho boas respostas para o exposto acima. Mas parece que o software não pode ser provado porque é arte e não ciência. Como você prova um Picasso?