История изменений
Исправление AndreyKl, (текущая версия) :
Так проблема в том, что Coq считает, что функция возможно бесконечна. Если же мы любую функцию будет преобразовывать в вычисления с ограниченным числом итераций, то реально зависающая функция будет проходить проверку и пойдёт в работу как проверенная. А потом на каких-то данных обрушит систему.
Нет, это неверно. Я ведь объяснил: доказываешь функциональную корректность, потом доказываешь нужные свойства. Если всё докажешь, ничего никуда не упадёт.
Ну либо пишешь и доказываешь свойства того что написал. Тогда тоже не упадёт, ты ж доказывал о том что написал.
Исправление AndreyKl, :
Так проблема в том, что Coq считает, что функция возможно бесконечна. Если же мы любую функцию будет преобразовывать в вычисления с ограниченным числом итераций, то реально зависающая функция будет проходить проверку и пойдёт в работу как проверенная. А потом на каких-то данных обрушит систему.
Нет, это неверно. Я ведь объяснил: доказываешь функциональную корректность, потом доказываешь нужные свойства. Если всё докажешь, ничего никуда не упадёт.
Исходная версия AndreyKl, :
Так проблема в том, что Coq считает, что функция возможно бесконечна. Если же мы любую функцию будет преобразовывать в вычисления с ограниченным числом итераций, то реально зависающая функция будет проходить проверку и пойдёт в работу как проверенная. А потом на каких-то данных обрушит систему.
Нет, это неверно. Я ведь объяснил: доказываешь функолнальную корректность, потом доказываешь нужные свойства. Если всё докажешь, ничего никуда не упадёт.