Почему писать корректный софт так тяжело — и математика тут не спасёт
Why Writing Correct Software Is Hard
Почему написать корректную программу принципиально сложно? Автор собирает воедино результаты теории вычислимости и теории сложности: от теоремы об остановке и теоремы Райса до функции занятого бобра, которая растёт быстрее любой вычислимой функции. Разбор показывает, что корректность — не вопрос правильных инструментов, а следствие фундаментальных законов вычислений. Отдельно упоминается машина Тьюринга на 1919 состояний, независимость от ZFC которой доказать невозможно.
Для математика не существует Ignorabimus, и, по моему мнению, для естествознания тоже. … Настоящая причина, по которой [никому] не удалось найти неразрешимую задачу, по моему мнению, в том, что неразрешимой задачи не существует. В противоположность глупому Ignorabimus наше кредо гласит: мы должны знать, мы будем знать!
- turbobutton
Я считаю, что существует жёсткое различие между абстрактной, математической корректностью в программном обеспечении и функционированием в реальном мире. Любой софт, который обрабатывает входные данные и предоставляет людям сложные рабочие процессы, неизбежно должен иметь дело с бесконечными капризами реальности.
Это не значит, что формальная корректность бесполезна, но важная часть — определить, когда она полезна, а когда доставляет больше хлопот, чем стоит...
- mpweiher
Я думаю, сначала нужно понять, что вообще такое «корректность».
Корректность относительно формальной спецификации?
Откуда мы знаем, что спецификация «корректна»? По определению?
- johnbender
Насколько я могу судить, статья ошибочно смешивает теорему Райса с идеей, что нельзя доказать что-то о маленькой программе, сгенерированной Йедидьей и Ааронсоном, но теорема Райса говорит не об этом. Вместо этого она говорит, что мы не можем придумать общий метод, чтобы правильно определять для всех программ, достигает ли программа заданной точки.
Для данной программы и разового доказательства можно доказать многое, или, если мы сделаем надприближение, предположив, что циклы завершаются, мы можем обоснованно доказать многое с риском отвергнуть программы, которые иногда корректны (например, системы типов).
Впрочем, это могло быть особенностью языка или моего восприятия.
- kodoman
Мне всегда была интересна формальная верификация, но я писал только игрушечные доказательства и производные программы.
Приятно видеть это старое обсуждение темы вне контекста «AI does lean» и предположений, что формальная верификация проста или будет простой для ИИ и можно просто отключить мозг.
Создание программ, которые можно верифицировать в принципе, — сложная задача проектирования, требующая настоящих размышлений и глубокого понимания проблемы.
- tromp
> машина Тьюринга с 1919 управляющими состояниями, которая не может быть доказана как завершающаяся (т.е. она «независима от ZFC»). Эта машина настолько мала, что легко помещается в 4K-челлендж
Одна маленькая придирка:
4K-челлендж обычно относится к коду, который помещается в 4КБ, но простая кодировка машины Тьюринга с 1919 состояниями занимает 19192(2+11) = 49894 бита, или 6237 байт, более 6КБ.
Однако недавние оптимизации на основе ИИ снизили количество состояний до не более чем 215, что легко помещается в 1КБ...
- nirinor
Самая важная часть негативного утверждения неявна: какие разумные допущения могут опровергнуть это утверждение?
Конечно, по теореме Райса, ни одна программа не может решить, всегда ли произвольная функция вычисляет сумму своих двух входов. Но это только потому, что мы допускаем сколь угодно сложные для анализа реализации функции суммы. Так что эта теорема сосуществует с тем фактом, что простые реализации суммы можно доказать корректными.
В этом свете, я думаю, лучший вывод: «чтобы писать корректный софт за разумное время, мы должны использовать легко анализируемые языки и стили программирования».
- bluGill
Настоящий вопрос: для типичной программы мы можем её доказать — даже хотя мы знаем, что есть программы, которые мы доказать не можем?
Меня не волнуют приведённые примеры, меня волнует мой текстовый процессор, веб-браузер и тому подобное. Можем ли мы доказать их — с ограничениями на язык сценариев?
- myrmidon
Мне показалось интересным, как нижняя граница для чемпиона BB(6) (бобёр-строитель с 2 символами и 6 состояниями) датирует статью: там указано >10^36534, но текущий чемпион (mxdys 2025) — это >10↑↑10↑↑10↑↑8 (10↑↑8 — это степенная башня 10^10^10^10... высотой восемь, и выражение вычисляется справа налево, так что 10↑↑10↑↑8 уже совершенно невообразимо велико).