
Представьте себе оркестр. сотен музыкантов. Каждый играет свою партию, свою мелодию. В одиночестве эти партии имеют смысл, но вместе они создают нечто большее — симфонию. А теперь представьте, что у этого оркестра нет дирижера и нет партитуры. Каждый музыкант начинает играть, когда хочет, и как хочет. Результат будет не музыкой, а оглушительным какофоническим хаосом.
В середине 1970-х годов мир компьютерных систем именно таким и становился. Появились процессоры, способные выполнять несколько задач одновременно. Сети, соединяющие сотни машин. Это был зарождающийся оркестр цифрового мира, и он стремительно скатывался в хаос. И тогда в Эдинбурге появился человек, который взял в руки пустой нотный лист и начал писать партитуру для этого безумия. Его звали Робин Милнер.
Артур Джон Робин Горелл Милнер родился 13 января 1934 года в Плимуте, на юго-западе Англии, в семье солдата. Его детство и юность пришлись на послевоенные годы, эпоху, когда Британия восстанавливалась и верила в силу науки и техники. Он показал блестящие способности к математике и поступил в Королевский колледж в Кембридже — один из академических центров мира.
В те годы информатика как самостоятельная дисциплина только зарождалась. Компьютеры были гигантскими, капризными машинами, а программирование было скорее искусством, чем наукой. Милнер же был математиком до мозга костей. Его привлекала не техника сама по себе, а элегантность и строгость логических систем. Он хотел найти не просто способ заставить машину что-то делать, а способ *доказать*, что она сделает это правильно.
Первый большой прорыв Милнера был связан с фундаментальным вопросом: как мы можем доверять сложной программе? Как математически доказать, что в ней нет скрытой ошибки, которая может привести к катастрофе, например, в системе управления ядерным реактором или в банковском ПО?
Работая в Университетском колледже Лондона, а затем в Эдинбургском университете, он создал систему под названием LCF (Logic for Computable Functions). Это был не язык программирования в привычном смысле. Это был скорее диалог, интеллектуальный поединок программиста с машиной. Программист выдвигал утверждение о своей программе («эта функция никогда не зациклится»), а система LCF требовала доказательства, шаг за шагом проверяя его логику.
Но чтобы создать этот инструмент для доказательств, Милнеру нужен был язык. И он его создал. Назвал его ML (Meta Language). Этот язык был настолько элегантным и мощным, что его «побочный эффект» оказался гораздо влиятельнее, чем основная цель. ML стал одним из первых языков программирования с так называемой автоматической выводимостью типов — система сама могла понять, какого типа данные обрабатывает программа, освобождая программиста от рутинных описаний. Идеи, заложенные в ML, легли в основу множества современных языков, таких как Haskell, OCaml и даже частично в F# и Scala. Он искал способ доказывать правильность программ, а по пути создал новый, более совершенный способ их написания.
Но главным делом его жизни, его великой партитурой для цифрового оркестра стало создание CCS (Calculus of Communicating Systems — Исчисление взаимодействующих систем). Это была не программа и не язык. Это был математический язык, чистая абстракция, предназначенная для одной цели: описывать, как независимые процессы общаются друг с другом.
В мире CCS все состоит из «процессов». Ваш веб-браузер — это процесс. Сервер, к которому он обращается — другой процесс. Каждая вкладка в браузере — тоже процесс. У каждого процесса есть свои действия. Но магия происходит в точке их взаимодействия, в «связи». Милнер создал простой, но невероятно мощный синтаксис для описания этих связей. Он показал, как можно анализировать сложные системы, разбивая их на простые, взаимодействующие части и изучая их «разговоры».
Это был революционный сдвиг. До этого программисты думали о программах как о последовательных инструкциях, как о рецепте. Милнер предложил думать о них как об экосистеме, как о сообществе агентов, которые постоянно обмениваются сообщениями. Его работа дала теоретикам и инженерам инструменты для борьбы с самыми сложными и коварными ошибками в параллельных системах — так называемыми «состояниями гонки», когда два процесса пытаются изменить одни и те же данные одновременно, приводя к непредсказуемым результатам.
Ум Милнера не стоял на месте. Он увидел, что его CCS хорош для описания систем с фиксированными «каналами» связи. А что если сами каналы могут создаваться и уничтожаться динамически? Этот вопрос привел его к созданию следующей, еще более мощной формальной системы — пи-исчисления.
За эти три столпа — LCF, ML и CCS/пи-исчисление — Робин Милнер в 1991 году получил высшую награду в мире компьютерных наук — премию Тьюринга. Для широкой публики это имя ничего не значило. В мире же программистов и теоретиков это было событие, равное присуждению Нобелевской премии физику-теоретику.
Робин Милнер ушел из жизни 20 марта 2010 года в Кембридже. Он был тихим, скромным человеком, глубоким мыслителем и блестящим наставником. Он никогда не создавал продуктов, которые можно было бы купить в магазине. Он не основывал стартапов и не давал громких интервью. Его наследие невидимо, но оно повсюду. Оно в стабильности операционных систем на вашем телефоне, в надежности серверов, обрабатывающих финансовые транзакции, в самой способности наших устройств делать несколько дел одновременно.
Он был тем самым человеком в тени, который написал партитуру для цифрового оркестра. И каждый раз, когда вы слушаете музыку в наушниках, пока в фоновом режиме скачивается файл и обновляется приложение, и все это работает без сбоев, — в этот момент вы слышите тихую, но уверенную мелодию, сочиненную Робином Милнером.
Робин Милнер за работой. Фото с сайта theguardian.com
| Родился: | 13.01.1934 (76) |
| Место: | Плимут (GB) |
| Умер: | 20.03.2010 |
| Место: | Кембридж (US) |