Габриэла Морейра, генеральный директор Quint в Informal Systems – Интервью

Габриэла Морейра, генеральный директор Quint в Informal Systems, является исследовательским инженером, специализирующимся на языках программирования и формальных методах, с сильным акцентом на создании инструментов, которые делают проверку сложных систем более доступной для инженеров. Она руководит разработкой Quint, современного исполняемого языка спецификаций на основе TLA+, где она продолжает поддерживать и развивать язык и его инструменты. Ее работа охватывает формальную верификацию, статический анализ и инструменты для разработчиков, и она также внесла свой вклад в академию, преподавая формальные методы, что отражает сочетание практической инженерии и теоретической глубины.

Quint, разработанный и поддерживаемый в Informal Systems, является современным языком спецификаций, предназначенным для моделирования, тестирования и верификации сложных систем, таких как распределенные сети, блокчейны и базы данных. Основанный на фундаменте темпоральной логики действий (TLA), Quint вводит более дружественный синтаксис для разработчиков, а также продвинутые инструменты, такие как проверка типов, симуляция и модельная проверка, что позволяет инженерам обнаруживать системные сбои до развертывания. Платформа подчеркивает исполняемые спецификации, что позволяет разработчикам не только описывать поведение системы, но и активно тестировать и исследовать его, мостя разрыв между теоретической правильностью и реализацией в реальном мире.

Вернувшись к началу, что первым вызвало ваш интерес к программированию, и как вы в конечном итоге нашли свой путь в формальные методы и распределенные системы?

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

В 2015 году я была представлена программными конкурсами. В них вы обычно получаете несколько примеров входных и ожидаемых выходных данных, и вы пишете код, который решает проблему и работает для этих примеров. Однако после того, как вы отправите его на оценку, код фактически тестируется на многих более примерах, чем те, которые показаны вам. Это осознание того, что код может работать для сценариев, которые я вижу или думаю, но все равно может не работать в случаях, которые я не рассмотрела, сделало программирование своего рода вызовом, в который я влюбилась.

Работая в отрасли, я быстро была привлечена к распределенным системам, где нам приходилось учитывать разные порядки сообщений, которые могут прибыть, разные режимы сбоя и целый мир скрытого поведения. В 2018 году коллега представил мне формальный язык спецификаций под названием TLA+. Я была увлечена. Я сразу начала строить инструменты вокруг TLA+ и с тех пор работаю в этой области.

Вы построили свою карьеру вокруг формальных методов и языков программирования, от вашей ранней работы над инструментами на основе темпоральной логики действий (TLA+) до руководства разработкой Quint в Informal Systems. Что мотивировало вас сосредоточиться на том, чтобы сделать формальную верификацию более доступной, и как это видение сформировало дизайн Quint?

TLA+ слишком хорош, чтобы не использовать его широко в отрасли. Я была еще довольно младой, когда узнала о нем, и я присоединилась к звонкам с моими коллегами, чтобы попытаться придумать решения вместе, и я постоянно находила сценарии, в которых наши решения не работали. Однако я всегда была последней линией защиты против этих сценариев в большинстве случаев. Я поняла, что должно быть лучший, менее дорогой и более ценный способ решить эти сценарии. Таким образом, идея использования формальных методов для создания спецификаций до реализации кода была создана. Итак, я начала свое академическое путешествие к этому, которое привело меня в Informal Systems и Quint.

Quint не был первоначально задуман как продукт. Мы построили его из необходимости в Informal Systems. Мы писали спецификации TLA+ для систем, которым мы доверяли больше, чем делали, но это не расширилось за пределы очень небольшой группы людей, поскольку синтаксис был слишком страшным с слишком многими математическими символами, и инструменты не соответствовали базовым ожиданиям людей. Мы показывали коллегам и внешним сотрудникам: “посмотрите на это удивительное, что я сделал”, но они не могли его прочитать и не имели времени, чтобы выучить новый инструмент.

Дизайнерские решения в Quint следуют напрямую из этого опыта. Язык легко читается и запоминается. Первое, что мы построили, было расширение VSCode, которое выделяет ошибки при наборе текста. У него есть типы и различные режимы, чтобы явно разделить слои. У него есть REPL, чтобы можно было исследовать интерактивно, и симулятор, чтобы можно было получить быструю обратную связь и итерировать. Он экспортирует трассировки в стандартизированный формат JSON, который легко парсируется машинами. Это были вещи, которые программисты уже ожидали от своих инструментов и которые нам были нужны сами. Верификация под ним является той же логикой, что и TLA+.

Я увлечена тем, чтобы сделать формальные методы более доступными, и выпуск инструментов – это интересно, но реальное влияние ощущается только в том случае, если команды инженеров фактически используют их. Есть еще разрыв между тем, что могут сделать инструменты, и тем, насколько они полезны для разработчиков, и я работаю над тем, чтобы закрыть этот разрыв.

Для читателей, незнакомых с этим, как бы вы объяснили, что такое Quint и почему был нужен новый язык спецификаций наряду с существующими инструментами, такими как TLA+?

Большинство спецификаций – это документация. Вы пишете, что должна делать система, и вы проверяете их, читая их. Проблема в том, что документация может быть неправильной в способах, которые нельзя механически обнаружить: неопределенные имена, двусмысленное поведение, неявные предположения. Вы обычно обнаруживаете это во время реализации или в производстве.

Спецификация Quint – это то, что можно выполнить. Вы моделируете систему как машину состояний, определяете свойства, которые она должна удовлетворять, и запускаете или проверяете модель. Если есть нарушение, вы получаете контрпример, показывающий точно последовательность шагов, которая вызывает его. Это меняет, когда и как дешево вы обнаруживаете ошибку дизайна.

TLA+ всегда мог это делать. Quint делает это практичным для инженеров, которые не являются уже специалистами в темпоральной логике.

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

Честно говоря, самым большим барьером на доступности был синтаксис. Вот почему мы начали с синтаксиса. После того, как мы решили эту проблему, мы могли сосредоточиться на других факторах. Система типов и эффектов Quint добавляет ограничения, но ограничения, которые полезны. Они предотвращают целый класс ошибок спецификаций, которые не весело находить после того, как проверка уже запущена. Типы почти полностью выводятся, и эффекты скрыты от пользователей, поэтому это добавляет ценность без трения.

Самое большое влияние после этого было наше симулятор. Он начался как способ предложить людям первую обратную связь о поведении их системы, как разработчик хочет иметь возможность как-то запустить код после его написания. Затем оказалось, что это крайне ценно как способ получить уверенность в спецификациях, которые слишком велики для проверки, поскольку экспертиза адаптации спецификации для того, чтобы сделать ее возможной для проверки, не должна приниматься как должное. Наш симулятор сделал уверенность более доступной, и мы использовали его обширно во многих проектах.

Моя самая большая боль при работе с синтаксисом TLA+ была в том, как часто я смешивала обратные слэши и обычные слэши, и вам нужно набирать их много. Мне нравится синтаксис Quint больше, но то, что действительно делает его невозможным вернуться для меня, – это все инструменты.

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

Самый большой сдвиг – это перемещение проверки на более раннюю стадию. Лесли Лэмпорт, создатель TLA+, сравнивает написание спецификаций до кода с созданием чертежей до строительных работ. Даже если вы уже построили что-то без чертежа, все равно хорошо написать его сейчас и использовать его для информирования ваших дальнейших изменений.

В отрасли программного обеспечения мы используем файлы markdown и доски. Может быть, вы можете сравнить это с попыткой описать здание текстом. Это работает, но знаете ли вы, сложатся ли размеры стен? Quint предлагает способ описать системы, где вы можете быть так же высокоуровневым, как хотите, и получить представление о его поведении и правильности.

Quint строится на фундаменте TLA+, который широко используется для описания распределенных систем. Как вы сбалансировали сохранение этой теоретической строгости, делая язык более дружественным для разработчиков?

Ключевым решением было ограничить Quint фрагментом TLA (логикой за TLA+), а не раскрыть все, что позволяет логика. TLA очень выразительна, и часть этой выразительности включает операторы, которые не поддерживаются никакими инструментами, и позволяет комбинациям, которые люди понимают и используют неправильно, что делает все действительно трудным для отладки. Мы приняли намеренное решение: придерживаться того, что большинство реалистичных спецификаций фактически нуждаются, и избегать того, что имеет потенциал для путаницы.

Система типов и система эффектов добавляют ограничения, но ограничения, которые полезны. Они предотвращают целый класс ошибок спецификаций, которые не весело находить после того, как проверка уже запущена. Типы почти полностью выводятся, и эффекты скрыты от пользователей, поэтому это добавляет ценность без трения.

Прежде чем я узнала о существовании TLA+, я занималась исследовательской работой в системах типов, что означает, что проверка типов Quint, вероятно, была моим любимым компонентом для написания. Я помню, как пила кофе с вкусом Paçoca в мои первые несколько месяцев в Informal, просматривая некоторую статью о системе типов и думая: “моя жизнь удивительна”.

Сделать язык хорошим для использования, сохраняя при этом соответствие TLA+ (поскольку спецификации Quint можно транслировать в TLA+), было упражнением в языке программирования, и обсуждения с командой были наиболее полезным ресурсом, за которым последовала обратная связь от ранних пользователей. Еще есть улучшения, которые мы хотим сделать, и это, возможно, моя любимая часть работы.

Вы также работали над статическим анализом и системами типов. Как этот опыт повлиял на проверку типов Quint, инструменты и общий опыт разработчика?

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

Функциональное программирование было представлено мне очень рано, я выучила Haskell в то же время, что и C (мой первый язык программирования), и я очень благодарна за это. Это основа, которая помогает мне видеть, что изоляция мутаций состояния и неопределенности в тонком слое в Quint, и наличие всей сложности в чистых функциях объективно помогает во многих факторах, и это не только вопрос вкуса. Я не думаю, что построение Quint было бы продуктивным, если бы вопросы вкуса часто обсуждались.

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

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

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

Существует растущий интерес к сочетанию ИИ с разработкой программного обеспечения. Видите ли вы роль ИИ в помощи разработчикам писать, проверять или даже генерировать формальные спецификации с помощью инструментов, таких как Quint?

Значительную, и это уже происходит. Компьютерная наука больше, чем написание кода, и ИИ открывает двери к совершенно новым способам использования формальных методов. Модели языка являются хорошими для написания спецификаций Quint из естественно-языковых описаний системы и даже существующего кода. Набор LLM Quint имеет агенты Claude Code, которые принимают английское описание протокола и производят спецификацию Quint, которую можно запустить и проверить сразу.

В то же время Quint также помогает разработчикам доверять коду, написанному с помощью ИИ. Я твердо верю, что уверенность должна прийти от понимания, а не от каких-то магических галочек. Работа над спецификацией Quint, которая управляет и проверяет код реализации, означает, что разработчики все равно могут владеть и понимать поведение системы, решая когнитивный долг, который может создать использование ИИ, и предоставляя более уверенные способы проверки сгенерированного кода.

Мы используем модели языка как инструменты языка, которые пишут точные определения Quint из естественно-языковых намерений, и затем предоставляем инструменты Quint ИИ, чтобы он мог выполнить вещи, которые он не может надежно сделать самостоятельно, такие как нахождение краевых случаев.

Взглянув вперед, что должно произойти, чтобы формальные методы перешли от нишевого внедрения в стандартную часть жизненного цикла разработки программного обеспечения?

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

С ИИ, меняющим то, чем является наша профессия, по крайней мере до некоторой степени, я надеюсь, что это изменение будет в сторону более высокоуровневых дизайнерских решений и правильности поведения, что сделает формальные методы инструментом повседневного использования; и не к тому, чтобы мы не понимали ни один код или системы больше и проводили все свое время, просматривая код, сгенерированный ИИ, без каких-либо инструментов, чтобы помочь нам рассуждать о нем.

Спасибо за проницательное интервью; читатели, интересующиеся изучением этого исполняемого языка спецификаций для моделирования и верификации сложных систем, включая его инструменты и то, как начать, могут изучить Quint.