Почему компьютерная программа не может быть доказана так же, как математическое утверждение? Математическое доказательство построено на других доказательствах, которые построены от еще большего количества доказательств и вплоть до аксиом - тех истин истин, которые мы считаем самоочевидными.
Компьютерные программы, похоже, не имеют такой структуры. Если вы пишете компьютерную программу, как получается, что вы можете взять предыдущие проверенные работы и использовать их, чтобы показать истинность вашей программы? Вы не можете, так как ничего не существует. Далее, каковы аксиомы программирования? Самые атомные истины поля?
У меня нет хороших ответов на вышесказанное. Но кажется, что программное обеспечение не может быть доказано, потому что это искусство, а не наука. Как ты докажешь Пикассо?