Если вы пользовались LaTeX, то, возможно, знаете, что приставка «La» в названии проекта означает «Lamport» в честь разработчика этого набора макрорасширений для TeX. Однако Лесли Лэмпорт получил известность не только благодаря своему вкладу в развитие систем компьютерной верстки.Лесли Лэмпорт родился 7 февраля 1941 года в Бруклине. Его отец появился на свет в Российской империи, в городе Волковыск (ныне — Республика Беларусь), а мать была уроженкой Австро-Венгрии (сейчас ее родной город располагается на территории Польши). Лесли окончил школу в Бронксе, а затем поступил в Массачусетский технологический институт, где последовательно получил степень бакалавра и магистра в области математики, а впоследствии — доктора философии (Ph.D.) в Университете Брандейса.
Еще будучи аспирантом, Лесли устроился на работу в Massachusetts Computer Associates в качестве научного сотрудника в сфере информационных технологий. Именно там у молодого ученого-математика проснулся интерес к компьютерам, который он пронес через всю свою жизнь.
В 1977 году Лесли Лэмпорт присоединился к компании Digital Equipment Corporation (DEC), где впервые познакомился с системой верстки электронных документов TeX, разработанной Дональдом Эрвином Кнутом в 1978 году. Кнут создал TeX прежде всего потому, что не был удовлетворен качеством верстки его собственных книг. Предложенная им технология подготовки макетов публикаций стала революционной для своего времени, и ее вскоре взяли на вооружение не только в Addison-Wesley, но также в крупных университетских издательствах, таких как Cambridge University Press и Oxford University Press.
Отличительными особенностями TeX являются его открытый исходный код и кроссплатформенность. Платформонезависимость обеспечивает одинаковое воспроизведение созданных с помощью TeX документов в различных операционных системах и на разном оборудовании. А свободный доступ к исходному коду облегчил разработчикам процесс совершенствования этой технологии. В TeX реализован мощный язык макросов, с помощью которых можно определять пользовательские команды и стили. Такая расширяемость позволяет создавать документы со специфическим форматированием и автоматизировать повторяющиеся задачи.
В DEC Лэмпорту приходилось редактировать и писать значительные объемы документации, прежде всего, руководства, упрощающие составление программ и описание алгоритмов. Поэтому широко используемый для верстки TeX показался ему крайне полезным инструментом, хотя и не совсем удобным. Лесли взялся за создание макросов, расширявших и дополнявших стандартные возможности TeX — в первую очередь в попытке решить его собственные задачи. Он стремился упростить процесс верстки документов таким образом, чтобы пользователи могли сосредоточиться на содержании, не вникая в тонкости форматирования. Так и появился на свет LaTeX.
Философия LaTeX основана на идее «Что видишь, то и подразумеваешь» (WYSIWYM), в отличие от более распространенного подхода «Что видишь, то и получаешь» (WYSIWYG). Такое различие позволяет пользователям сосредоточиться на смысле содержимого, оставляя системе все детали представления. Пользователи составляют документы из обычного текста, вставляя в него команды, определяющие структуру и стили форматирования. Этот подход не только упрощает процесс написания, но и обеспечивает последовательность и согласованность всего документа.
LaTex можно использовать для создания различных типов документов — от научных статей и диссертаций до презентаций и резюме. Причем технология доступна пользователям разного уровня: начинающие могут применять базовый набор команд для стандартного форматирования, а к услугам более опытных — широчайший ассортимент инструментов, позволяющих адаптировать документы к своим потребностям. Исходный код системы находится в свободном доступе, что позволяет создавать для LaTex различные готовые шаблоны и приложения, облегчающие процесс форматирования и редактирования файлов. Для верстки в формате LaTeX можно использовать практически любой текстовый редактор, хотя существует и множество специализированных программ, значительно облегчающих разметку.
Изначально Лесли Лэмпорт не планировал представлять свой проект широкой публике, но редактор издательства Addison-Wesley Питер Гордон убедил его написать развернутое руководство по практическому использованию LaTex. Именно этот момент и стал отправной точкой роста популярности LaTex не только в Северной Америке, но и по всему миру. Книга «LaTeX: A Document Preparation System» была опубликована в 1986 году и быстро превратилась в международный бестселлер, а сама технология стала стремительно превращаться в один из наиболее распространенных стандартов представления электронной документации, сделавшись важным инструментом для ученых, математиков и технических писателей.
21 августа 1989 года Лэмпорт передал права на дальнейшую разработку и поддержку LaTex группе пользователей TeX из Стэнфорда под руководством Фрэнка Миттельбаха. Группа носит название TeX Users Group (TUG), и именно она занялась дальнейшим развитием технологии и выпуском исправлений.
Распределенные вычислительные системы и сети оставались основным направлением исследований Лэмпорта, в ходе которых он стремился разработать набор правил, способных упростить и систематизировать эту область. В конце 1970-х — начале 1980-х годов Лэмпорт сформулировал алгоритм Paxos — фундаментальную концепцию распределенных систем. Этот алгоритм заложил основу для достижения консенсуса в сети ненадежных вычислителей. Предложенную Лэмпортом идею автоматного подхода в распределённых вычислениях можно назвать критически важной разработкой для функционирования современных компьютерных сетей. Он предложил метод реализации алгоритма в распределённых системах, сохраняющий устойчивость к отказам. На основе концепций Лэмпорта в начале 90-х было разработано семейство протоколов для выполнения распределенных транзакций.
Как говорил сам Лэмпорт в одном из своих интервью, «Распределенная система — это система, в которой сбой компьютера, о существовании которого вы даже не подозреваете, может сделать вашу собственную машину непригодной для использования». Повышению надежности таких систем он и посвятил свои исследования. Принято считать, что работы Лэмпорта сделали возможным создание облачных инфраструктур таких глобальных провайдеров, как Google и Amazon. Кроме того, его идеи нашли применение в современных реализациях искусственного интеллекта. За свой вклад в систематизацию поведения распределенных систем Лэмпорт стал лауреатом Премии Тьюринга 2013 года — самой престижной премии в сфере компьютерных технологий.
Лэмпорт является одним из создателей алгоритма Чанди–Лэмпорта для определения непротиворечивых глобальных состояний и автором «Подписи Лэмпорта» — одного из прототипов цифровой подписи, которые используются сегодня повсеместно для валидации электронных документов. Кроме этого, он известен своими работами по темпоральной логике, в частности, в качестве изобретателя временной логики действий (Temporal logic of actions, TLA). Эта логика используется для описания поведения параллельных и распределенных систем. Если несколько компьютеров выполняют вычисления в перекрывающиеся промежутки времени, может возникнуть неопределенность, связанная с разными показаниями часов в этих системах. Для решения подобных коллизий Лэмпорт предложил использовать идеи специальной теории относительности, в результате чего на свет появилась концепция «логических часов», также называемых «часами Лэмпорта».
На основе своей разработки Лэмпорт создал язык спецификаций TLA+, опирающийся на теорию множеств и темпоральную логику действий. В частности, этот инструмент позволяет использовать математические доказательства для проверки правильности программного кода, а также описывать точные алгоритмы проектирования сложных программных систем. По словам самого Лэмпорта, этот язык можно рассматривать в качестве «донкихотской попытки преодолеть антипатию инженеров к математике».
Чтобы объяснить предназначение TLA+, Лэмпорт прибегал к аналогиям из мира кулинарии: если разработка простой программы не сложнее процесса варки куриного яйца, то большой проект сродни организации банкета, в ходе которого на стол в разное время подают множество блюд и напитков. TLA+ позволяет описать процесс приготовления этих блюд и сервировки стола так, чтобы каждому гостю подавались правильные порции в нужном порядке, и в ходе мероприятия не возникло досадных ошибок и недоразумений. TLA+ использует спецификации в качестве входных данных, и проверяет, будут ли они работать так, как задумано. Лэмпорт с иронией утверждал, что инженеры-программисты часто приступают к работе над проектом, не убедившись, что его реализация возможна с учетом изначальных требований, имеющихся инструментов и ресурсов, в то время как ни один повар не начнет готовить блюда для банкета, если не уверен, что у него есть достаточный запас продуктов, а рецепт может быть воплощен на практике.
Основы языка и теории временной логики действий Лесли Лэмпорт описал в своей книге «Спецификация систем: язык TLA + и инструменты для инженеров аппаратного и программного обеспечения» (Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers). Правда, язык все же не нашел широкого применения в индустрии. Сам его создатель объясняет это следующим образом: «Современные проекты делаются в спешке. Есть старая поговорка: «Некогда сделать все правильно. Но всегда есть время все переделать». Поскольку TLA+ требует предварительных усилий, вы добавляете новый шаг в процесс разработки программного обеспечения, а это сложно продать».
В 2001 году Лесли Лэмпорт покинул группу компаний DEC/Compaq, и присоединился к исследовательскому центру Microsoft Research в Калифорнии в качестве разработчика-исследователя. За свой вклад в развитие компьютерных технологий Лэмпорт был удостоен звания почетного профессора и доктора в нескольких европейских университетах: в Университете Ренна, Университете Кристиана Альбрехта в Киле, а также в Университете Лугано и Университете Нанси. Кроме того, Лесли Лэмпорт является членом множества международных компьютерных ассоциаций. В 2011 году он был избран членом Национальной академии наук США.
Как и многие другие известные ученые в области IT, Лесли Лэмпорт начал свой путь в сферу компьютерных технологий с математики. Тем не менее, он не оставил свою основную стезю, и сумел объединить математический научный подход с вычислительной техникой, благодаря чему на свет появился не только стандарт LaTeX, который активно используется по всему миру и по сей день, но также революционный алгоритм Paxos, ставший краеугольным камнем в области распределенных вычислений. Способность Лэмпорта соединять миры математики и информатики говорит о его широчайшем кругозоре и гениальности, как технического специалиста, и как ученого. А его готовность свободно делиться своими идеями, проявившаяся в открытом исходном коде LaTeX, внесла значительный вклад в развитие электронной документации и технической литературы в середине 80-х годов.
Статья поддерживается командой Serverspace.
Serverspace — провайдер облачных сервисов, предоставляющий в аренду виртуальные серверы с ОС Linux и Windows из любой точки мира менее чем за 1 минуту. Для построения ИТ-инфраструктуры провайдер также предлагает: создание сетей, шлюзов, бэкапы, сервисы CDN, DNS, объектное хранилище S3.
