Буду говорить в контексте программирования, но соображения можно распространить шире.
Когда мы описываем алгоритм: программу, доказательство теоремы или решение математической задачи — мы строим его описание в рамках некоторой формальной модели. В рамках соглашений и ограничений, которые мы явно или неявно принимаем.
Описать алгоритм вне формальной модели невозможно. Хотя бы потому, что любой язык — уже формализация.
Отсюда вытекает интересная проблема.
Привет.
В посте Тесты, которые тестируют тесты я описал свой взгляд на верификацию программ через дублирование их логики в виде отдельной модели и последующее сравнение с ней. В качестве частного случая выступили юнит-тесты.
В этот раз, опираясь на изложенные идеи, я попробую сформулировать общий подход к оценке уровня верифицированности ПО.