Такие доказательства были сложными и трудоемкими, но они были доказательствами. С их развитием идея создания евклидовой иерархии теорем выглядела достижимой в реальности.
Объявление вредным
В 1968 году Дейкстра написал редактору журнала CACM письмо под заголовком Go To Statement Considered Harmful («О вреде оператора Go To»)
[10], которое было опубликовано в мартовском выпуске. В статье он обосновал свою позицию в отношении трех управляющих структур
[11].
И мир программирования запылал. Тогда у нас не было Интернета, поэтому люди не могли публиковать злобные мемы на Дейкстру и затопить его недружественными сообщениями. Но они могли писать — и писали — письма редакторам многих популярных журналов.
Не все письма были корректными. Некоторые из них были резко отрицательными; другие выражали решительную поддержку. И эта битва продолжалась почти десять лет.
В конце концов спор утих по одной простой причине: Дейкстра победил. По мере развития языков программирования инструкция goto все больше сдавала свои позиции, пока, наконец, не исчезла. Большинство современных языков программирования не имеют инструкции goto, а некоторые, такие как LISP, никогда ее не имели.
В настоящее время все программисты используют парадигму структурного программирования, хотя и не всегда осознанно. Просто современные языки не дают возможности неограниченной прямой передачи управления.
Некоторые отмечают сходство инструкции break с меткой и исключений в Java с инструкцией goto. В действительности эти структуры не являются средствами неограниченной прямой передачи управления, имевшимися в старых языках, таких как Fortran или COBOL. Кроме того, даже языки, сохранившие ключевое слово goto, часто ограничивают возможность переходов границами текущей функции.
Функциональная декомпозиция
Структурное программирование дает возможность рекурсивного разложения модулей на доказуемые единицы, что, в свою очередь, означает возможность функциональной декомпозиции. То есть решение большой задачи можно разложить на ряд функций верхнего уровня. Каждую из этих функций в свою очередь можно разложить на ряд функций более низкого уровня, и так до бесконечности. Кроме того, каждую из таких функций можно представить с применением ограниченного набора управляющих структур, предлагаемых парадигмой структурного программирования.
Опираясь на этот фундамент, в конце 1970-х годов и на протяжении 1980-х годов приобрели популярность такие дисциплины, как структурный анализ и структурное проектирование. В тот период многие, например Эд Йордан, Ларри Константин, Том Демарко и Меилир Пейдж-Джонс, продвигали и популяризовали эти дисциплины. Следуя им, программисты могли разбивать большие системы на модули и компоненты, которые затем можно было разбить на маленькие и доказуемые функции.
Формальные доказательства отсутствуют
Но доказательства так и не появились. Евклидова иерархия теорем не была построена. И программисты не увидели преимуществ использования трудоемкого процесса формального доказательства правильности каждой, даже самой маленькой функции. В конечном итоге мечта Дейкстры рассеялась как дым. Не многие из современных программистов считают, что формальные доказательства являются подходящим способом производства высококачественного программного обеспечения.
Конечно, формальный евклидов стиль математических доказательств не единственная стратегия создания чего-то правильного. Другой, более успешной стратегией является научный метод.
Наука во спасение
Принципиальное отличие науки от математики заключается в том, что правильность научных теорий и законов нельзя доказать. Я не смогу доказать верность второго закона движения Ньютона, F = ma, или закона гравитации, F = Gm1m2/r2. Я могу продемонстрировать действие этих законов и провести измерения, подтверждающие их правильность до многих знаков после запятой, но я не смогу доказать их в математическом смысле. Я могу провести массу экспериментов и собрать массу эмпирических подтверждений, но всегда остается вероятность, что какой-то эксперимент покажет, что эти законы движения и гравитации неверны.
Такова природа научных теорий и законов: их можно сфальсифицировать, но нельзя доказать.
Тем не менее мы верим в эти законы. Каждый раз, садясь в автомобиль, мы ставим свою жизнь на то, что формула F = ma точно описывает окружающий мир. Каждый раз, делая шаг, мы ставим свои здоровье и безопасность на верность формулы F = Gm1m2/r2.
Наука не требует доказательства истинности утверждений, чаще она требует доказательства их ложности. Утверждения, доказать ложность которых не удается после многих усилий, мы считаем истинными.
Конечно, не все утверждения требуют доказательств. Например, утверждение «это — ложь» не является ни истинным, ни ложным. Это один из простейших примеров утверждений, не требующих доказательств.
Подводя итог, можно сказать, что математика — это дисциплина доказательства истинности утверждений, требующих доказательства. Наука, напротив, — дисциплина доказательства ложности утверждений, требующих доказательства.
Тестирование
Однажды Дейкстра сказал: «Тестирование показывает присутствие ошибок, а не их отсутствие». Иными словами, тестированием можно доказать неправильность программы, но нельзя доказать ее правильность. Все, что дает тестирование после приложения достаточных усилий, — это уверенность, что программа действует достаточно правильно.
Следствия из этого факта могут показаться ошеломляющими. Разработка программного обеспечения не является математической задачей, даже при том, что она связана с применением математических конструкций. Эта сфера деятельности больше похожа на науку. Мы убеждаемся в правильности, потерпев неудачу в попытке доказать неправильность.
Такие доказательства неправильности можно применить только к доказуемым программам. Недоказуемую программу — например, из-за неумеренного использования goto — нельзя считать правильной, сколько бы тестов к ней ни применялось.
Парадигма структурного программирования заставляет нас рекурсивно разбивать программы на множество мелких и доказуемых функций. В результате мы получаем возможность использовать тесты, чтобы попытаться доказать их неправильность. Если такие тесты терпят неудачу, тогда мы считаем функции достаточно правильными.
