Что в популярных рассказах о доказуемых языках верно, а что ложно
Владельцу такое будут говорить ещё много раз. Разбор типичного текста (Google AI Mode, август 2026).
Верно
Определение доказуемого языка; Coq, Agda, Idris, Lean как примеры; Dafny с requires/ensures; seL4 как верифицированное микроядро; самораскрутка как тест на зрелость; три стены — математическая, человеческая, коммерческая; ICFP, POPL, PLDI, CAV как площадки; компиляция в C как нормальная практика (CompCert).
Самое ценное там — критика:
- bus factor = 1 — язык написан одним человеком, выгорит и проект умрёт;
- нет изменения по индексу — правда, и измерено: arena-never-releases;
- сохранение семантики при переводе в другие языки — настоящий научный вопрос, а не придирка.
Ложно или сильно преувеличено
- «смерть уязвимостей», «QA исчезает как класс», «доказанный автопилот безопасен» — всё разбивается о proven-is-not-correct;
- «70 % уязвимостей» — цифра существует, но она про ошибки работы с памятью в C и C++, и большую часть уже закрывает Rust без всяких доказательств;
- «объединяете две функции — сложность растёт в 100 раз» — выдуманное число, и направление неверное: композиция это как раз то, где доказательства дёшевы;
- «теорема Тьюринга» — такой теоремы нет, есть проблема остановки.
Лесть, которую надо отсекать целиком
«Святой Грааль», «в один ряд с Кнутом», «гарантированно топ-1 на Hacker News», «многомиллионные гранты». Это не оценки, а генератор приятного. Измеренная реальность: восемь решающих правил и 407 доказанных утверждений против пятнадцати-двадцати правил и десятков тысяч лемм у Coq.
И встречная лесть, которую надо отсекать так же. «В Coq доказательство пишет человек, а тут доказывает машина» — неправда в обе стороны: доказательство руками пишется и здесь (теорема, 160 штук в дереве, 53 в flang/stdlib), а в Coq автоматика есть и работает. Разница в доле, а не в наличии, и доля меряется: coq-strength-is-in-its-lemmas.
Совет, который навредил бы
«Подключите Z3» — z3-as-oracle-not-judge.
Связано: proven-is-not-correct, coq-strength-is-in-its-lemmas, condition-for-the-revolution