¿Por qué no se puede probar un programa de computadora como lo hace una declaración matemática? Una prueba matemática se construye sobre otras pruebas, que se construyen a partir de más pruebas y hasta axiomas, esas verdades verdades que sostenemos como evidentes.

Los programas de computadora no parecen tener esa estructura. Si escribe un programa de computadora, ¿cómo es que puede tomar trabajos probados anteriores y usarlos para mostrar la verdad de su programa? No puedes ya que ninguno existe. Además, ¿cuáles son los axiomas de la programación? ¿Las verdades muy atómicas del campo?

No tengo buenas respuestas a lo anterior. Pero parece que el software no se puede probar porque es arte y no ciencia. ¿Cómo se prueba un Picasso?