Без заголовка
> Затраты же времени и сравнение по эффективности невозможны, ибо разные люди имеют производительность в кодировании на разных языках на порядки разные (т.е. мы измерим тем самым разницу интеллектов людей, а не производительность метода верификации/тестирования).
Пока к сожалению затраты на верификацию очень велики. Асимптотически (по мере увелеичения тестового покрытия) верификация конечно же эффективнее тестирования. Т.е. затраты на тестирование пропорциональны количеству тест-кейсов, а на верификацию - фиксированные, ибо это полный перебор. Т.е. в какой-то момент верифицировать достаточно сложный код будет дешевле, чем полнсотью тестировать (что часто невозможно). Но сейчас на практике, это бывает крайне редко.
Мне кажется это вызвано несовершенством инструментария. Т.е. мое ощущение, что если современные технологии правильно настроить, то эффективность верификации будет сравнима с тестированием на задачах типа создания серверов. Пока однако пользоваться доступным инструментарием очень не просто - ибо рассуждать в терминах логики программистам неудобно. Я вот подумываю над разработкой нотации, приближенной к программированию, чтобы все работа велась на языке близком программисту. Тогда будет сильно проще.