Лесли Лампорт: «Алгоритм без доказательства — это лишь догадка»

Quanta Magazine 3,5 млн 7 мин 2 мин 17.05.2022
Главное

Лесли Лампорт — выдающийся ученый в области компьютерных наук, чья карьера стала мостом между чистой математикой и практической инженерией. В видео, подготовленном Quanta Magazine, он рассказывает о том, как математический подход к проектированию алгоритмов и понимание принципов причинно-следственной связи легли в основу современных распределенных систем.

🧠 Математический взгляд на программирование 0:03

Лесли Лампорт, чей путь в науку начался с изучения математики, утверждает, что компьютерные науки в привычном понимании на заре его карьеры практически не существовали. По его мнению, одна из ключевых ошибок в индустрии заключается в путанице между «программированием» и «кодингом».

По мнению Лампорта, обучение программированию через «обучение кодингу» равносильно обучению писательскому мастерству через обучение набору текста на клавиатуре, что лишает процесс интеллектуальной глубины. Хотя инженерам бывает сложно освоить математический подход, он убежден, что именно это развивает способность мыслить системно и строго.

🌐 Революция в распределенных системах 2:50

Распределенная система — это среда, где выход из строя одного компьютера может сделать бесполезной всю сеть, даже если вы не подозревали о существовании этого узла. Интерес Лампорта к этой области возник случайно, после прочтения препринта статьи Роберта Томаса и Пола Джонсона, посвященной реализации распределенных баз данных.

Для поддержания консистентности данных в распределенных системах Лампорт применил знания теории относительности:

  1. Причинность: В специальной теории относительности разные наблюдатели могут по-разному определять одновременность событий, но понятие причинно-следственной связи («событие А произошло до события Б») является инвариантным.
  2. Критика алгоритма: Лампорт заметил, что алгоритм Томаса и Джонсона нарушает эту фундаментальную концепцию причинности.
  3. Машина состояний: Решением проблемы, по словам Лампорта, стало создание так называемой «машины состояний» — абстрактного компьютера, который выполняет по одной операции за раз, заставляя все узлы сети работать согласованно.

Эта концепция стала фундаментальной для того, как современные инженеры проектируют сложные распределенные архитектуры.

🏭 Вдохновение в индустрии и «пекарный алгоритм» 5:17

Лампорт сравнивает свою исследовательскую работу с живописью Огюста Ренуара. Если пытаться придумывать задачи в отрыве от реальности, их количество ограничено, но в реальном производстве существуют миллионы уникальных проблем, ждущих своего решения.

Особое место в его творчестве занимает «пекарный алгоритм» (bakery algorithm), предназначенный для решения задачи взаимного исключения (mutual exclusion) — например, чтобы два процесса не пытались воспользоваться принтером одновременно.

💬 Цитаты

«Люди путают программирование с кодингом. Кодинг — это то же самое для программирования, что печатание для письма.»

Лесли Лампорт 01:12

«Алгоритм без доказательства — это догадка, это не теорема.»

Лесли Лампорт 00:44
👥 Спикер
🔗 Упомянутые сайты и проекты
📖 Термины
Распределенная система
Компьютерная система, состоящая из множества независимых узлов, которые взаимодействуют друг с другом для выполнения общей задачи.
TLA+
Язык спецификации высокого уровня, разработанный Лесли Лампортом для моделирования и проверки сложных систем до их реализации.
Взаимное исключение
Задача в информатике, заключающаяся в предотвращении одновременного доступа нескольких процессов к общему ресурсу.
Машина состояний
Абстрактная модель, которая выполняет операции последовательно, обеспечивая согласованность данных в распределенной системе.
📊 Цифры
⚖️ Другая сторона
Математика и физика Leslie Lamport distributed systems TLA+ bakery algorithm