Бибер выходит на сцену Coachella: миллионы, мерч и личное видение
11.04.2026 01:21:54
15 ноября 2018 года Ксавье Лерой прочёл вступительную лекцию в Коллеж де Франс. Он стал первым, кто занял только что учреждённую кафедру программных наук в одном из старейших академических учреждений Европы.
Для человека, который признаётся, что в детстве программирование было для него «скучным и одновременно захватывающим», это особое место финала. Коллеж де Франс — где лекции открыты для всех и где нет студентов, только мыслители — подходит для него точнее, чем любой обычный университет.
Но путь туда занял тридцать один год. И начался — с Apple II в детской комнате.
Как многие из его поколения, в подростковой комнате Ксавье Лерой впервые познакомился с вычислительной техникой.
«Тогда только начинались персональные компьютеры, и их возможности были крайне ограничены... Но я помню, как пытался писать небольшие программы. Это было весело, но прежде всего — раздражающе!» — рассказывал он в интервью. — «Я был преимущественно самоучкой, пользовался журналами и несколькими книгами. Потом пошёл изучать математику и физику на подготовительных курсах».
Пикантная деталь: настоящее увлечение компьютерной наукой пришло не от Apple II, а позже. «Я влюбился», — признавался он, — «только во время первого курса в ЭНШ, когда открыл для себя фундаментальную информатику — захватывающую вселенную высокой формальной чистоты».
В 1987 году Лерой был принят в Эколь Нормаль Сюперьёр в Париже, где изучал математику и информатику.
Сам он называл ЭНШ так: «церковь французской математики». «Туда попасть было признанием. И там я открыл для себя фундаментальную информатику».
ЭНШ — особое учреждение в французской академической системе. Не университет в обычном смысле, а инкубатор интеллектуальной элиты: математиков, философов, учёных. Конкурс жесточайший. Те, кто поступает, — как правило, те, кто определит облик своей дисциплины на несколько десятилетий.
В стенах ЭНШ он встретил традицию, уходящую корнями к Робину Мильнеру и его языку ML. «Всё это было привезено во Францию моим научным руководителем Жераром Юэ около 1980 года. Он начал работать с эдинбургским ML Мильнера и решил, что это хороший язык реализации для его работы по автоматическому доказательству теорем — работы, которая несколько лет спустя даст нам Coq».
В 1989 году Лерой получил степень магистра фундаментальной информатики в Парижском университете 7, а в 1992 году — докторскую степень по той же специальности под руководством Жерара Юэ.
Тема диссертации — типовые системы для семейства языков ML. Это был вход в сердце теоретической информатики: строгие математические гарантии того, что программа ведёт себя так, как задумал программист — до запуска, во время компиляции.
После стажировки в Кремниевой долине он стал членом совместной команды ЭНШ и Inria Рокенкур «Формель» для докторантуры по типовым системам семейства языков ML, после чего вернулся в США — на этот раз в Стэнфорд.
В 1991 году Лерой совместно разработал Caml Light — лёгкую реализацию с интерпретатором байт-кода и эффективным поколенческим сборщиком мусора, заложившую основу для последующих разработок.
Это привело к распространению языка, особенно во Франции — для обучения программированию.
К 1995 году он представил Caml Special Light, добавив компилятор нативного кода для повышения производительности и сложную систему модулей, вдохновлённую Standard ML, обеспечивавшую раздельную компиляцию и функторы для модульной организации кода.
После постдокторантуры в Стэнфордском университете Лерой в 1994 году стал научным сотрудником Inria.
«У меня появились новые идеи для системы модулей. У Дидье Реми и Жерома Вуийона появились идеи для объектов и классов. Я также сделал кое-какую работу по компиляции в реальный машинный код. Сложив всё это вместе, мы получили OCaml».
Современный OCaml появился в 1996 году с выпуском Objective Caml 1.00, созданного Лероем совместно с Жеромом Вуийоном, Дамьеном Долижем и Дидье Реми и включавшего объектно-ориентированное расширение при сохранении функционального ядра.
Помимо руководства разработкой OCaml с 1995 по 2012 год, его основными вкладами были дизайн и реализация системы модулей, а также двух компиляторов: простого, но эффективного байт-кодового компилятора и оптимизирующего компилятора нативного кода, генерирующего высокопроизводительный ассемблерный код для различных платформ.
История OCaml — это история постепенного выхода академического языка в промышленность.
«Поначалу пользователи были преимущественно академическими. Потом появились пользователи из промышленности. Началось с Microsoft Research, делавшей несколько важных проектов на OCaml, и нескольких других мест, потом — Jane Street Capital, использующая его для всей своей инфраструктуры и вкладывающая в него огромные ресурсы».
Среди организаций, использующих OCaml: Facebook (Flow, Hack, Infer, Pfff, Reason), Bloomberg (BuckleScript), Citrix Systems (XenServer), Jane Street Capital — ведущая компания в области пропритарной торговли, сделавшая OCaml своим основным языком.
«Я провёл несколько лет, доводя OCaml до совершенства. Распространяемый в версии 5.0 в 2022 году, он доступен с открытым исходным кодом и может использоваться для разработки приложений с очень высокими гарантиями безопасности и надёжности. После применения в промышленности (авиация, космос и ядерная отрасль) мы сейчас наблюдаем его использование для приложений, связанных с системным программированием, блокчейном и финансовыми вычислениями».
В конце 1990-х годов Лерой сделал необычный шаг — из чистой науки в стартап.
В конце 1990-х годов Ксавье Лерой заинтересовался компьютерной безопасностью и провёл несколько лет в стартапе Trusted Logic, специализирующемся в этой области.
Работая вместе с основателем Доминик Больяно, он выполнял роль научного консультанта: «Мне тогда было 32 года, что делало меня одним из старших членов команды, где динамизм и творчество были необходимым условием».
«В 2004 году я вернулся в Inria на полную ставку и, опираясь на то, что узнал в Trusted Logic, погрузился в мир формальных методов, сосредоточившись на верификации критического программного обеспечения — такого, как используемое в смарт-картах, а также в системах управления электронными самолётными средствами, метро без машинистов и атомными электростанциями».
Этот пятилетний опыт дал ему нечто, чего не давала академия: понимание того, как программное обеспечение работает в условиях, где ошибка стоит не репутации, а жизней.
Возвращение в Inria совпало с новым, самым амбициозным проектом в его карьере.
«Я решил сделать полный бэкенд — от простого нетипизированного C до ассемблера PowerPC. Это было тяжело. Это было моё первое большое доказательство в Coq. Оно насчитывало, наверное, 20 000 строк на тот момент, но в итоге сработало. Это привело к моей первой публикации по теме на конференции POPL 2006».
Суть CompCert: компилятор — это программа, переводящая исходный код на языке высокого уровня в машинный код. Любой баг в компиляторе может привести к тому, что машинный код не будет соответствовать намерениям программиста. «Точно так же, как неправильная интерпретация при переводе между естественными языками меняет смысл текста, баг в компиляторе может заставить его производить машинный код, не соответствующий намерениям исходной программы».
CompCert решает эту проблему радикально: он математически доказан — с помощью системы Coq/Rocq — быть корректным. Он является руководителем проекта CompCert, разрабатывающего оптимизирующий компилятор для языка C, формально верифицированный в Rocq (прежнее название: Coq).
«CompCert получил широкое признание в академическом сообществе. У меня есть серия статей, которыми я чрезвычайно горжусь. Он также привлёк интерес промышленности. Мне довелось работать с людьми из Airbus, заинтересованными в использовании CompCert в производстве. Я многому научился у них в области высоконадёжного программного обеспечения».
В мае 2018 года Лерой был назначен профессором Коллеж де Франс и занимает кафедру программных наук.
Исследования Ксавье Лерой направлены на использование строгих математических подходов для повышения безопасности, защищённости и удобства разработки критически важного программного обеспечения. С одной стороны, он изучает новые языки программирования и инструменты, основанные на функциональной парадигме; с другой — формальную верификацию критического программного обеспечения методами дедуктивной верификации и статического анализа.
В ноябре 2025 года он опубликовал черновик готовящейся книги «Управляющие структуры в языках программирования: от "goto" до алгебраических эффектов».
Награды накапливались методично — как строки доказательства.
2007 год: премия «Мишель Монпети — Inria». 2011 год: премия La Recherche в категории информатики за проект CompCert. 2016 год: премия Мильнера Королевского общества «в знак признания его исключительных достижений в компьютерном программировании». 2018 год: Большая премия Inria — Французской академии наук.
В декабре 2022 года он был избран членом Академии наук Института Франции.
В январе 2023 года вместе с соавторами он получил премию ACM SIGPLAN Programming Languages Software Award за CompCert. В январе 2024 года — премию ACM SIGPLAN Programming Languages Software Award за OCaml. «После более чем 30 лет работы над Caml это было удовольствием и честью — стоять на сцене на POPL 2024 вместе с несколькими другими ключевыми разработчиками OCaml для получения этой награды».
«Некоторые занимаются академической информатикой, чтобы убежать от программирования. Я определённо не из таких».
Это, пожалуй, лучший автопортрет. Профессор Коллеж де Франс, член Академии наук, лауреат множества наград — и человек, который по-прежнему пишет код.
Его исследовательские интересы охватывают типовые системы, компиляцию, верификацию байт-кода, семантику языков, языковую безопасность и системы модулей.
Apple II в подростковой комнате в 1980-х. Математические курсы, ЭНШ, Жерар Юэ. Caml Light, затем OCaml. Пять лет в стартапе. 20 000 строк доказательств компилятора. Коллеж де Франс. Академия наук.
В феврале 2026 года он продолжает читать лекции — на этот раз о безопасных вычислениях: вычислениях на зашифрованных или приватных данных.
Человек, который доказал компилятор, продолжает доказывать — что фундаментальная наука меняет мир.
Фото с сайта inria.fr
| Родился: | 15.03.1968 (58) |
| Место: | Орлеан (FR) |
