Published on
Updated on 

Интервью с Ксавьером Лерой

Authors

  • Эта публикация - перевод статьи. Ее автор - People of Programming Languages. Оригинал доступен по ссылке ниже:

    Interview with Xavier Leroy

Xavier Leroy - старший научный сотрудник INRIA, интересующийся научными аспектами программирования. Он возглавляет группу Gallium по разработке, формализации и реализации языков и систем программирования. Известен как основной разработчик языка программирования OCaml и компилятора. В этом интервью мы поговорим о создании OCaml, взаимосвязи между программированием и исследованиями, а также о влиятельной работе Ксавье над CompCert, формально верифицированным компилятором языка Си.

JY: Расскажите о себе.

XL: Я вырос во Франции. Я немного знаком с персональными компьютерами, как их называли в 1980-х годах, в частности, с любимым Apple 2. Именно там я изучал программирование. В основном я был самоучкой, используя журналы и несколько книг. Я продолжал изучать математику и физику в подготовительных классах. Меня приняли в ENS, Высшую нормальную школу в Париже, которая является церковью французской математики. Я очень хотел заниматься математикой. Потом я узнал, что математика оказалась сложнее, чем я думал. Их курсы были действительно трудными, и они не делали их очень доступными. Они хотели найти следующего Филдсовского медалиста. В то же время я получил свои первые курсы по информатике. В ENS они открыли учебную программу по CS за год до этого, в 86 году. Я нашел их чрезвычайно интересными, потому что они имели смысл, объясняли некоторые тайны программирования Apple 2, а также демонстрировали очень хорошую математику.

Я влюбился в то время, а затем продолжил обучение в магистратуре и аспирантуре по теоретической информатике в Париже. Несколько стажировок научили меня многому: в частности, стажировка у Луки Карделли в центре системных исследований Digital Equipment. Затем я стал постдоком в Стэнфорде. Затем меня взяли на работу в INRIA, и я до сих пор работаю в INRIA.

Когда я еще колебался между математикой и информатикой, в Политехническом институте проходил однодневный семинар о прикладной математике в современном мире. Один из моих преподавателей сказал мне: "Ну, почему бы тебе не пойти? Может быть, ты чему-нибудь научишься".

Один из докладчиков был руководителем программы для космической ракеты Ariane 4. Не той 5, которая взорвалась при первом запуске, а предыдущей. Он говорил: "О, да. Мы использовали много очень хорошей математики для ее проектирования. А также довольно много программного обеспечения. 100 000 строк кода, и мы очень гордимся всем этим".

Кто-то из аудитории спросил: "А как вы уверены, что ваши строки кода делают то, что вы думаете?".

Он ответил: "Мы очень тщательно их протестировали".

Даже в то время казалось, что этого недостаточно. Я знаю, что Ariane 4 работала, но тот же самый код был использован в Ariane 5 и привел к тому, что первый запуск прошел бурно. Помню, тогда я подумал, что, наверное, с программным обеспечением нужно делать что-то большее, чем просто тестировать его.

JY: Как появилась CompCert?

XL: Как я пришел к работе над CompCert, я разговаривал с одним человеком из отраслевого отдела исследований и разработок. Его зовут Эммануэль Лединот. Он возглавлял отдел исследований и разработок французской компании Dassault Aviation, производящей самолеты. Они производят истребители и бизнес-джеты.

Эта группа была связующим звеном между Dassault Aviation и французскими академическими исследованиями в течение двадцати лет. Я знал его, потому что они использовали Caml для некоторых своих внутренних инструментов. Однажды, наверное, в 2003 году, я встретил его на приеме на конференции, и он сказал мне: "У нас много проблем с нашими компиляторами C. Согласно правилам, мы должны проводить много проверочных мероприятий в компиляторе, чтобы убедиться, что он не вносит ошибок. Это очень трудно сделать, потому что компилятор - это черный ящик, и потому что иногда мы используем оптимизацию, и она все портит".

Он сказал: "Может быть, есть какое-то формальное доказательство, которое можно сделать для компилятора Си".

Эта идея зародилась у меня в голове, и через год у меня появилось свободное время. Я сказал: "Хорошо, давайте я попробую смоделировать в Coq простую оптимизацию. Просто простой промежуточный язык и распространение констант. Посмотрим, как это будет выглядеть".

На самом деле это выглядело довольно хорошо. Некоторые другие коллеги из INRIA, например Ив Берто, тоже заинтересовались. В какой-то момент я решил сделать полноценный бэкенд из минорного языка Си. Очень простой нетипизированный язык C к языку ассемблера PowerPC. Это было сложно. Это было мое первое действительно большое доказательство Coq. В то время оно было, возможно, 20 000 строк, но в итоге оно сработало. Это привело к моей первой публикации на эту тему на POPL 2006. Затем, после этого, я смог, с некоторыми коллегами, добавить другие части. Самой трудной частью, безусловно, была семантика языка Си и работа почти со всем языком Си. Си - это обманчивый язык. В то время я программировал на C уже 20 лет, поэтому я думал, что знаю его. Нет. Я знал только то небольшое подмножество, которое регулярно использовал. Я до сих пор обнаруживаю странные положения в стандартах языка Си.

CompCert рос и был очень хорошо принят в академическом сообществе. У меня была серия работ, которыми я очень горжусь. Он также вызвал некоторый интерес со стороны промышленности, но пока не очень большой. Все это занимает много времени. Мне довелось поработать с некоторыми людьми в Airbus, которые заинтересованы в использовании CompCert в производстве. От них я узнал много нового о программном обеспечении высокой надежности.

JY: Я также хотел бы поговорить о том, как появился OCaml. Какова была мотивация? Ожидали ли вы, что это будет язык, который будут преподавать во французских школах?

XL: [Смеется.] Нет. Это довольно долгая история. Я не первый в этой истории. Она восходит к Милнеру и его "ML", "метаязыку" для его провера, и этому подходу функционального языка, специфичного для конкретной области, встроенного в среду Lisp и имеющего систему типов. Все это было привезено во Францию моим советником Жераром Юэтом (Gérard Huet) около 1980 года. Он начал играть с эдинбургским ML, ML Милнера. В какой-то момент он решил, что это будет хорошим языком реализации для его работы по автоматическому вычислению - работы, которая через несколько лет привела к появлению Coq. До этого он, как и все остальные, реализовывал на Lisp. В то время все в сообществе символьных вычислений работали на Lisp.

Он оценил звучность типов и так далее. У него и нескольких коллег, таких как Гай Кузино, который также был одним из моих учителей в ENS, возникла идея новой реализации под названием Caml. Это был вариант Edinburgh ML с новой реализацией, которая не переводила на Lisp, а переводила непосредственно на виртуальную машину. Caml происходит от ML и CAM - категориальной абстрактной машины: виртуальной машины, вдохновленной декартовыми замкнутыми категориями.

Это дало нам первый Caml. Именно с ней я играл, когда был студентом в ENS. Она работала на мини-компьютерах, таких как Vax, и на дорогих рабочих станциях. Он был довольно тяжелым для того времени. Чтобы запустить ее, нужно было не менее 8 мегабайт оперативной памяти! В частности, она не работала на персональных компьютерах или чем-то подобном. Он был практически непригоден для преподавания и для многих приложений. Я познакомился с этим во время своей первой стажировки.

Затем, с другим другом из ENS, Дамьеном Долигезом, мы подумали, что, возможно, мы могли бы сделать лучшую, более легкую реализацию, используя виртуальную машину, вдохновленную Smalltalk-80, и современный сборщик мусора. Таким образом, это был интерпретатор виртуальной машины, написанный на C, а затем компилятор для довольно небольшого языка ML. Приложив некоторые усилия, его удалось запустить на персональных компьютерах. Это был 1990 год.

В преподавание он попал благодаря Вероник Донзо-Гуж и Терезе Хардин, которые вели большой курс программирования в CNAM. Затем он был выбран для подготовительных занятий. Внезапно у нас появилось довольно много пользователей, в основном студенты, а также некоторые ученые. В США это началось в то время в таких местах, как UPenn и Cornell, а также немного в Японии, в частности, в Киото.

Затем через несколько лет появился OCaml. Я защитил докторскую диссертацию и вернулся ко всему этому, когда меня взяли на работу в INRIA. У меня были новые идеи по поводу системы модулей. У Дидье Реми и Жерома Вуйона были идеи по поводу объектов и классов. Я также проделал некоторую работу по компиляции в реальный машинный код. Если собрать все это вместе, получился OCaml. Первоначально пользователями были в основном академики. Затем у нас появилось несколько пользователей в промышленности. Это началось с Microsoft Research, который сделал пару важных проектов на OCaml, и нескольких других мест, затем Jane Street Capital, которая использовала его для всей своей инфраструктуры и действительно вкладывает в него много ресурсов.

JY: Некоторые люди занимаются академической информатикой, чтобы убежать от программирования, но похоже, что вся ваша карьера была связана с программированием. Какова связь между вашей практикой программирования и вашими исследованиями?

XL: Действительно, я не убегаю от программирования. Я рассматриваю свои исследования как один из способов лучше понять программирование. Мне нравится иметь цели исследования, которые я могу использовать в своем программировании. Например, реализованный язык программирования или семантика, которую я могу использовать, чтобы рассуждать о своем коде. Это делает меня очень чувствительным к инструментам. Не только к принципам, но и к инструментам, которые реализуют их на практике.

JY: Как вы решаете, над какими проблемами работать?

XL: Я стараюсь быть открытым и смотреть, какие проблемы есть у людей - практиков или ученых. Связи с программным обеспечением и практикой программирования всегда привлекательны для меня. Я вижу себя как человека, пытающегося служить и защищать программное обеспечение.

JY: Какие, по вашему мнению, наиболее интересные или важные проблемы, на которых сообщество может или должно сосредоточиться в ближайшие несколько лет?

XL: Возможно, пришло время вернуться к проектированию языков программирования и попытаться проявить немного больше воображения. В 90-х годах мы думали, что новый PL решит все наши проблемы, а сегодня мы склонны думать, что мы здесь для того, чтобы разрабатывать инструменты верификации для старых языков. Может быть, нам стоит немного вернуться к языкам, специфичным для конкретного домена. Меня раздражает то, как трудно программировать массивно параллельные вычисления. В частности, с GPU высокопараллельное оборудование стало очень доступным, но мы по-прежнему программируем его с помощью диалектов языка C и некачественных инструментов.

Затем, конечно же, машинное обучение. В настоящее время многие приложения в основном изучаются на примерах, а не пишутся на основе первых принципов. Это вызов для нас, людей, владеющих языками программирования. Я, конечно, понятия не имею, как применять формальные методы к таким приложениям, как связать проверку модели или доказать, что состояние недостижимо. Даже традиционное тестирование сталкивается с проблемой: вы можете тестировать эти системы, полученные путем обучения, но как измерить покрытие тестов? Когда эти системы используются только для сортировки моих фотографий или распознавания моего голоса, небольшая ошибка здесь и там не убьет меня. Но когда говорят об автомобилях без водителя, построенных на этой технологии, это заставляет меня нервничать.