“Real mathematicians don't prove.” EWD1012.
Грубо говоря, есть два способа рассуждать о программах, я называю их «аксиоматический метод» (postulational method) и «операционный метод» (operational method).
Первый метод называется «аксиоматическим» потому, что утверждение о том, что программа соответствует спецификации, и сопутствующие леммы выводятся из программного текста так же, как математическая теория выводится из аксиом. (Исчисление предикатов оказалось незаменимым средством в эффективном построении доказательства этого утверждения.) При использовании аксиоматического метода мы рассматриваем текст программы как математический объект сам по себе, то есть семантическая эквивалентность двух программ означает, что они удовлетворяют одной и той же спецификации.
Второй метод называется «операционным» потому, что он требует анализировать вычисления, которые выполняет программа, и требует доказать, что каждое вычисление совместимо с данной спецификацией. Он опирается на модель вычислений, которая нужна, чтобы интерпретировать текст программы как исполняемый код.
Трагедия современного программирования в том, что, даже если оно и рассуждает о программах, то исключительно операционно. Я считаю это трагедией, потому что с чисто технической точки зрения операционный метод на несколько порядке хуже аксиоматического метода. По мере роста размера и сложности программы применять операционный метод становится невозможно, и всеобщая привязанность к операционному мышлению является причиной того, что разработка ПО завязла в кризисе.
Пожалуй, один из фундаментальных изъянов операционного метода — то, что он не отвечает на вопрос, как рассуждать об алгоритмах. Он транслирует действия одного алгоритма в действия другого алгоритма, например, интерпретатора программ (то есть абстрактной машины, которая реализует модель вычислений). сейчас мы не будем рассматривать этот потенциально серьёзный недостаток. мы рассмотрим прагматический аспект: включая — может, лучше сказать: генерируя? — в наше рассмотрение все возможные вычисления, мы открываем дверь перед комбинаторным взрывом, который быстро исчерпывает наши силы. [Вспомните типичное оправдание программиста, внёсшего баг в программу: «Да ладно, он проявляется только в очень редких случаях».] Легче не бороться с последствиями комбинаторного взрыва, а предотвратить его; именно так и поступает аксиоматический метод, не рассматривая текст программы как исполняемый код. аксиоматический метод превращает текст программы в синтаксическое дерево, но не интерпретирует его дальше.
Противодействие аксиоматическому методу так же старо, как и его пропаганда; это было вполне предсказуемо. Проиллюстрирую:
Мораль сей басни такова: реальные программисты не рассуждают о программах, потому что это не круто. Они извлекают заменитель интеллектуального удовольствия из непонимания того, что они пишут, из безответственности и последующего вылавливания багов. Багов, которых нужно не вылавливать, а не допускать в самом начале.
* * *
Описанная выше война хорошо знакома любому человеку, хоть раз касавшемуся методологии программирования. Я заговорил о ней, потому что та же самая война пылает по всей математике: «формалисты» хотят развивать математику, манипулируя неинтерпретированными формулами по явно описанным правилам, а «антиформалисты» (informalist) — правда, сами они не называют себя таким негативным именем, скорее всего, они видят себя «настоящими математиками» — постоянно интерпретируют формулы и «рассуждают» в модели, которая подстилает формулы.
Продемонстрировав «прагматические примеры творческой мощи аксиоматического метода», Эрик Темпл Белл продолжает: «Математики и учёные традиционного склада иногда думают, что наука, втиснутая в рамки явно сформулированного множества посылок, утратила свою свободу и чуть ли не умирает. Практика показывает, что она утратила только одну вещь — привилегию делать ошибки в рассуждениях, которых можно было бы избежать. Люди везде остаются людьми, поэтому каждое новое наступление аксиоматического метода воспринимается как посягательство на священную традицию и встречает яростное сопротивление. Борьба с методом — это не больше и не меньше, чем борьба с математикой». Последнее предложение ясно показывает, какое занятие Белл считал достойным называться математикой. Он не относит себя к «математикам традиционного склада».
Давайте для контраста перечислим некоторых из них: Филип Дэвис и Рубен Херш. Они говорят, что «собственно математику (то, что настоящие математики делают в настоящей жизни) по ошибке отождествляют с её моделью или представлением в метаматематике или, если вам угодно, логике первого порядка». В следующем абзаце — знакомые слова — они догматически утверждают, что «такие [формальные] выводы [в логике первого порядка] являются чисто гипотетической деятельностью (за исключением «игрушечных» проблем, в которые можно сыграть в логике)». В следующем предложении они говорят о «настоящей математике, чьи доказательства подтверждены «консенсусом экспертов». Машина неспособна проверить настоящее доказательство…» Если Белл (в 1940 году) говорил о математике как о цели, Дэвис и Херш (1981) ссылаются на усреднённый статус-кво, включая все средневековые реликты.
У Дэвиса и Херша мне не нравится то, что их статус-кво очень близок к их цели. Они соглашаются, что «учитель может обучать математике, исследователь может написать статью, не обращая внимания на проблему интуиции», но это непременно «глупо и противоречит их собственным интересам». Моё предварительное заключение:
(Так говорит опыт. Я не рассчитываю, что мне удастся кого-нибудь убедить.)
Консенсусная модель математики побудила Алана Джея Перлиса и других заявить, что разработка программ, которые соответствуют спецификации на основании доказательства — недостижимая цель. Но они упустили из виду, что информатика, пожалуй, один из наименее средневековых разделов математики, разумеется, не «настоящей математики»!
* * *
Почему в математике, в противоположность другим наукам, — я имею в виду «настоящую математику, которой занимаются настоящие математики в настоящей жизни» — до сих пор хорошо и обильно сохранились средневековые реликты — это вопрос социологу науки. (Например, люди впитывают из окружающей среды знания о том, как строить математику, в традициях ремесленных гильдий, этому не учат явно. Даже во всех отношениях респектабельные профессора математики оправдываются тем, что другого пути нет.)
У меня не хватает знаний, чтобы предложить убедительное объяснение. Возрождение было болезненным поворотом для интеллектуальной элиты того времени. (Смотри судьбу Галилео Галилея.) Наука в сегодняшнем понимании слова родилась во время Возрождения (и подрастала в течение Просвещения), и интеллектуальная элита Средневековья — теология и математика — вынуждена была приспосабливаться. Теологам — по крайней мере, папству — понадобилось почти четыре столетия, чтобы окончательно очистить их религиозное учение от претензий на научность. Похоже, что математика в ещё более трудном положении. Её отделение от науки невозможно из-за её полезности. (Следует заметить, что формалисты смогли уйти от мутного метафизического понятия «истины» благодаря тому, что сконцентрировали внимание на доказуемости. Это было крупным достижением: вспомним, что не далее как в предыдущем столетии математика всё ещё страдала от сильного загрязнения философией, из-за чего даже сам Карл Фридрих Гаусс рассудил, что будет умнее не публиковать открытие неэвклидовой геометрии и пустить под артиллерийский обстрел Бойяи и Лобачевского.)
Другие науки начинали свою жизнь или могли начать жить с чистого листа во время Возрождения, а на математике висели гири результатов, полученных в течение многих столетий до Средневековья, которые в определённом смысле были полезными. Неудивительно, что в то время математика уцепилась за Эвклида.
Но это историческое объяснение не оправдывает того факта, что сегодня геометрию Эвклида, зная все её изъяны, изучают как прототип строго дедуктивной системы. Не оправдывает. То, что она сильно опирается на чертежи, считают подтверждением ценности «геометрической интуиции», тогда как на самом деле это является следствием изъянов аксиоматизации Эвклида. (К слову, я встречаю всё больше и больше случаев, подтверждающих, что именно неформальность рассуждений, опирающихся на чертежи, препятствует развитию эвристик, с помощью которых эти рассуждения можно построить в правильном порядке. Это являет собой резкий контраст с очень эффективными эвристиками, которые можно разработать для строго формального фундамента.)
Претенциозность, с которой учат геометрию Эвклида (то есть преподносят её как строго дедуктивную систему), — это большая бессовестная ложь. Всеобщая привычка верить этой лжи (и затем восхвалять «интуицию») говорит о многом: что математика остаётся дисциплиной со значительным донаучным компонентном, в котором позволено обитать призраку Средних веков.
Текст закончен в Остине 24 января 1988 года.