Когда идея написать о следующих пятидесяти годах компьютерных технологий впервые пришла мне в голову, я счёл её совершенно абсурдной: какой здравомыслящий ученый способен заглядывать так далеко в будущее? Но потом я понял, что преподаватели делают именно это постоянно: при разработке наших курсов мы решаем, что преподавать, а что игнорировать, и мы делаем это на благо людей, многие из которых будут по-прежнему активны через сорок-пятьдесят лет. Ясно, что какое-то видение следующего полувека компьютерной науки работает. К этому я должен добавить, что это нормально, если хрустальный шар будет слишком туманным, чтобы показать много деталей. Тридцать пять лет назад, например, я не имел ни малейшего представления о том, насколько тесно будут сочетаться замысел программы и замысел доказательства, и в таком смысле моя жизнь была полна сюрпризов. В то же время эти сюрпризы были событиями, которых я ждал, потому что я знал, что программирование должно быть превращено в дело, поддающееся некоторой математической обработке, задолго до того, как я знал, какой математикой это окажется. Другими словами, строя замки из песка на пляже, мы можем игнорировать волны, но должны следить за приливом.
* * *
К счастью, есть несколько вещей, которые мы можем извлечь из прошлого, например, что скорость, с которой общество может усваивать прогресс, строго ограничена, и это обстоятельство значительно упрощает долгосрочное прогнозирование. Ранее в этом десятилетии мне рассказали о великом изобретении под названием «окно регистра»; представляющий изобретение был очень молод, но для меня это изобретение показалось очень знакомым, потому что я вспомнил Burroughs B5000 тридцатилетней давности. Итак, если у вас есть яркая и здоровая идея, вы можете ожидать, что она будет провозглашена новинкой примерно к 2025 году.
Ещё одна вещь, которую мы можем извлечь из прошлого, - это провал таких характеристик, как «Компьютерная наука - это не что иное, как X», где вместо X вы можете заменить свою любимую дисциплину, например: численный анализ, электротехника, теория автоматов, теория массового обслуживания, лямбда-исчисление, дискретная математика или теория доказательств. Я упоминаю об этом из-за текущей тенденции приравнивать информатику к конструктивной теории типов или теории категорий.
Основная задача вычислительной техники - как не испортить её. Если люди возражают, что любая наука должна решать этот вызов, мы должны дать двойное опровержение. Во-первых, машины настолько быстры, а объемы хранения настолько огромны, что мы сталкиваемся с большим количеством путаницы, распространение которой легко непреднамеренно механизировать. Во-вторых, поскольку мы имеем дело с артефактами, вся неизученная сложность создается нами самими; винить больше некого, поэтому нам лучше научиться вообще не вводить сложность.
В этой связи показательна история компьютерного прерывания в реальном времени. Оно был изобретено с целью облегчения совместного использования процессора; его следствием стало введение недетерминизма и бесконечной головной боли для многих разработчиков операционных систем. Мы видели две реакции на это. Для отладки IBM построила специальные мониторы, которые точно записывали, когда центральный процессор обработал какое прерывание; когда что-то пошло не так, монитор можно было превратить в контроллер, заставив таким образом воспроизвести подозрительную историю и сделать «эксперимент» повторяемым. Другая реакция заключалась в том, чтобы определить условия, при которых можно было бы реально и безопасно рассуждать о недетерминированных программах, и впоследствии следить за тем, чтобы эти условия выполнялись как аппаратным, так и программным обеспечением. OS/360 навсегда после этого превратилась в беспорядок; мультипрограммная система THE, напротив, была настолько надежной, что ни одна неисправность системы никогда не вызывала ложных запросов на техническое обслуживание оборудования. Излишне говорить, что эта серия произвела на меня неизгладимое впечатление.
Одна мораль заключается в том, что прерывание в реальном времени было всего лишь волной, тогда как приливом было введение недетерминизма и системных инвариантов как средства борьбы с ним. Более широкая мораль - это конструктивный подход к проблеме корректности программы, к которому теперь мы можем добавить и проблему производительности системы. Спроектировать системы разделения ресурсов с такими взаимосвязанными стратегиями распределения слишком просто, что никакая прикладная теория очередей не предотвратит появления самых неприятных сюрпризов производительности. Разработчик, который считает предсказуемость производительности своей обязанностью, обычно создает проекты, которые вообще не нуждаются в теории очередей. Последний и на этот раз довольно недавний пример - конструкция нечувствительной к задержке схемы, которая делегирует все временные трудности в синхронизированных системах классу проблем, которых лучше избежать, чем решить. Мораль ясна: профилактика лучше лечения, особенно если болезнь неизлечима.
Приведенные выше примеры указывают на очень общую возможность, в широком смысле, которую можно охарактеризовать как проекты, в которых как конечный продукт, так и процесс проектирования отражают теорию, достаточную для предотвращения появления комбинаторного взрыва сложности. Есть много причин предполагать что эта возможность останется с нами в течение очень долгого времени, и это здорово для будущего компьютерной науки, потому что на протяжении всей истории упрощения оказывали гораздо большее научное влияние в долгосрочной перспективе, чем индивидуальные подвиги изобретательности.
Возможность упрощения очень обнадёживает, потому что во всех примерах, которые приходят на ум, процесс проектирования стоил намного меньше труда и приводил к гораздо лучшему конечному продукту, чем его интуитивно задуманные альтернативы. Таков мир, и я также надеюсь, что эта возможность останется с нами на десятилетия вперёд. Во-первых, простота и элегантность являются непопулярными, потому что они требуют напряжённой работы и дисциплины для достижения, а также образования, чтобы оценить. Во-вторых, мы наблюдаем массовые инвестиции в усилия, которые идут в противоположном направлении. Мне приходят на ум так называемые вспомогательные средства проектирования, такие как симуляторы схем, верификаторы протоколов, аниматоры алгоритмов, графические вспомогательные средства для разработчика оборудования и сложные системы для контроля версий: своим внушением мощности они скорее поощряют, чем препятствуют сложности. Вы не можете ожидать, что толпы людей, посвятившие значительную часть своей профессиональной жизни таким усилиям, будут любезно реагировать на предположение, что большая часть этих усилий была ошибочной, и вряд ли можно ожидать более сочувственного внимания со стороны грантовых агентств, которые финансировал эти усилия: было задействовано слишком много людей, и из прошлого опыта мы знаем, что то, что было достаточно дорого, автоматически объявляется большим успехом. В-третьих, представление о том, что автоматические вычисления не должны быть таким беспорядком, снова и снова затмевается появлением монстра, который впоследствии навязывается компьютерному сообществу в качестве стандарта де-факто (COBOL, FORTRAN, ADA, программное обеспечение для настольных издательских систем и т.д.).
Короче говоря, возможность упрощения останется у нас на долгие годы, и я предлагаю для сохранения нашего здравомыслия и энтузиазма, чтобы мы приветствовали долгую продолжительность этой возможности, а не страдали от нетерпения каждый раз, когда практикующие высмеивают и отбрасывают наш следующий успешный пилотный проект как игрушечную задачу: они сделают это, даже если вы достигли того, что незадолго до этого они уверенно предсказывали невозможным.
* * *
К настоящему времени мы все знаем, что программирование так же сложно или так же просто, как доказательство, и что если программирование процедуры соответствует доказательству теоремы, проектирование цифровой системы соответствует построению математической теории. Задачи изоморфны. Мы также знаем, что, хотя с операционной точки зрения программа может быть ничем иным, как манипулятором абстрактных символов, разработчику программы лучше рассматривать программу как сложную формулу. И мы также знаем, что есть только один способ создания сложных формул, заслуживающий доверия, а именно: вывод с помощью манипуляции с символами. Мы должны позволить символам делать свою работу, поскольку это единственная известная техника, которая может масштабироваться. Вычислительная техника и вычислительная наука неизбежно превращаются в упражнение в формальной математике или, если хотите, сокращенно: как упражнение в VLSAL (= Very Large Scale Application of Logic = очень крупномасштабное применение логики).
Из-за очень тесной связи между разработкой программ и разработкой доказательств любое продвижение в разработке программ имеет прямое потенциальное влияние на то, как выполняется общая математика. С тех пор, как учёные в области информатики создали компиляторы, они очень привыкли к идее механического манипулирования неинтерпретируемыми формулами, и я уверен, что они внесут значительный вклад в дальнейшую реализацию мечты Лейбница о представлении вычислений, то есть манипуляции с неинтерпретируемыми формулами, как альтернатива человеческому рассуждению. Однако задача воплотить эту мечту в реальность, безусловно, будет держать нас в напряжении не менее пяти десятилетий.
Дело не только в том, что создание соответствующей формальной, условной и концептуальной практики - это серьезная задача, которую ещё предстоит решить; это хуже, потому что нынешние традиции вряд ли могут помочь. Например, мы знаем, что переход от словесных рассуждений к формальным манипуляциям может быть оценён как сужение полосы пропускания для связи и документации, тогда как во имя «простоты использования» многие усилия компьютерного сообщества направлены на расширение этой полосы пропускания. Кроме того, мы знаем, что можем использовать систему только на основании наших знаний о её свойствах, и, аналогичным образом, уделяем как можно больше внимания выбору концепций, на основе которых мы строим наши теории: мы знаем, что должны сохранять чёткость, ясность и простоту, если не хотим быть раздавленными сложностями, созданными нами самими. Но, очевидно, рынок движется в противоположном направлении. Я до сих пор помню, как нашел книгу о том, как использовать Wordperfect 5.0, объемом более 850 страниц, фактически на дюжину страниц больше, чем мое издание Джорда Джуса «Теоретическая физика» 1951 года! Пора разоблачить компьютерное сообщество как тайное общество создания и сохранения искусственной сложности. А ещё у нас есть инженеры-программисты, которые упоминают формальные методы только для того, чтобы вызвать на них подозрение. Короче говоря, не следует ожидать слишком большой поддержки компьютерного сообщества в целом. И от математического сообщества я также научился не ожидать слишком большой поддержки, поскольку неформальность является отличительной чертой Математической гильдии, члены которой, подобно плохим программистам, получают интеллектуальное возбуждение от незнания того, что они делают, и предпочитают восхищаться чудесами человеческого разума (в частности, своего собственного). Для них мечта Лейбница - кошмар. Таким образом, мы сами по себе.
Но это не важно. В следующие пятьдесят лет математика превратится в искусство и науку эффективных формальных рассуждений, и мы будем получать интеллектуальное возбуждение от изучения того, как символы делают свою работу.
Calculemus!
(Примечание. Это адаптированная версия EWD1051.)
проф. д. Эдсгер В. Дейкстра
Кафедра информатики
Техасский университет в Остине,
Остин, Техас 78712-1188
США