А можете объяснить для чайника что эти гигабайты доказывают. Забудем про проблему остановки.
Вот одна программа сгенерировала гигабайты доказательства корректности сертифицируемой программы. Вторая программа проверила эти гигабайты и сказала, что всё в порядке.
Где гарантия, что ни в первой проверяющей программе ни во второй нет багов?
Где гарантия, что в исполняющем программы процессоре нет багов, что в процессе проверки не произошло ни одной ошибки чтения-записи памяти?
Как эти гигабайты убедят покупателя сертифицированной программы в том, что в ней нет багов?
