[prog] Не могу не выдернуть из контекста пассаж про верификацию программ

Персонаж с ником gandjustas у меня уже мелькал – цитировал я его высказывания с RSDN. С удовольствием сделаю это еще раз.

Итак, замечательная фраза:

Главное преимущество managed кода знаешь?
Это простая верифицируемость на клиенте. То есть непосредственно перед исполнением можно статически проверить что код не делает ничего криминального. Таким образом не нужны становятся аппаратные средства защиты, так как они рассчитаны на отлов тех же самых проблем, но в процессе исполнения.

На что его вполне резонно спросили:

А что именно значит "ничего криминального"? Если программа делит единицу на миллиардный по счету бит числа пи, как верификатор поймет, что там деление на ноль? Если идет обращение к массиву с нетривиально вычисляемым индексом, как верификатор угадает, нет ли выхода за пределы? Если идет загрузка модуля с вычисляемым именем и вызов функции из него, как статический верификатор узнает, что за функция будет вызвана?

И тут последовал совершенно феноменальный ответ:

Я с теорией верифцирования не сильно знаком, но верификация и сейчас производится.

И там же:

Верификация не обязана проверять твою программу на соотвествие спецификации (у верификатора чато и нету спецификации), но верификатор может проверить программу на отсутствие нарушений памяти, обращений по невалидным указателям итп.

Между тем понятие “верификация” является давно устоявшимся термином, который как раз таки обозначает доказательство соответствия кода программы исходной спецификации. Интересующихся отсылаю к Wikipedia и содержащимся там ссылкам:

Verification and Validation (software)
Formal methods

PS. Кстати говоря, то, о чем говорит gandjustas – проверка отсутствия обращения по неверным указателям, проверка отсутствия выхода за пределы массивов, перезапись переменных на стеке и пр. – вовсе не являются свойствами управляемого кода. Компилирующиеся в нативный код языки со сборкой мусора и контролем за массивами и отсутствием адресной арифметики (Oberon, Eiffel, OCaml и, отчасти, Ada) дают точно такую же безопасность. Может быть даже большую, поскольку Ada контролирует в run-time корректность преобразований типов (afaik, если вы объявите тип A как 1..10, а тип B как 5..11, и попробуете преобразовать значение 2 от типа A к типу B, то получите исключение в run-time).