Габріела Морейра, генеральний директор Quint у компанії Informal Systems – Серія інтерв’ю

Габріела Морейра, генеральний директор Quint у компанії Informal Systems, є інженером-дослідником, який спеціалізується на мовах програмування та формальних методах, з особливим акцентом на створенні інструментів, які роблять верифікацію складних систем більш доступною для інженерів. Вона очолює розробку Quint, сучасної мови специфікацій на основі TLA+, де вона продовжує підтримувати та розвивати мову та її інструменти. Її робота охоплює формальну верифікацію, статичний аналіз та інструменти для розробників, а також вона внесла свій внесок у науку, викладаючи формальні методи, що демонструє поєднання практичної інженерії та теоретичної глибини.

Quint, розроблений і підтримуваний у компанії Informal Systems, є сучасною мовою специфікацій, призначеною для моделювання, тестування та верифікації складних систем, таких як розподілені мережі, блокчейни та бази даних. Будучи заснованою на основі Temporal Logic of Actions (TLA), Quint вводить більш дружній синтаксис для розробників, а також просунуті інструменти, такі як перевірка типів, симуляція та модельна верифікація, що дозволяє інженерам виявляти системні збої до розгортання. Платформа підкреслює виконавчі специфікації, дозволяючи розробникам не тільки описувати поведінку системи, але й активно тестувати та досліджувати її, тим самим зменшуючи розрив між теоретичною правильністю та реальною реалізацією.

Повернувшись до початку, що спочатку спонукало ваш інтерес до програмування, і як ви врешті-решт знайшли свій шлях у формальні методи та розподілені системи?

Я була активною гравцем з поганим комп’ютером, і я зрозуміла, що мені подобається виправляти проблеми та робить його працездатним. Я записалася на комп’ютерні науки і була приваблена теорією та компіляторами.

У 2015 році мені були представлені програмні змагання. У них вам зазвичай дають кілька прикладів вхідних та очікуваних виходів, і ви пишете код, який розв’язує проблему та працює для цих прикладів. Однак після того, як ви надсилаєте його для оцінки, код насправді тестується з багатьма більшими прикладами, ніж ті, які їм показують. Це розуміння того, що код може працювати для сценаріїв, які я бачу або думаю, але все одно може зазнати невдачі в випадках, які я не розглянув, перетворило програмування на вид挑ання, в яке я закохалася.

Працюючи в галузі, я швидко була приваблена розподіленими системами, де нам доводилося考虑увати різні порядкування повідомлень, які могли надійти, різні режими збоїв та цілий світ прихованих поведінок. У 2018 році колега познайомив мене з формальною мовою специфікацій під назвою TLA+. Я була захоплена. Я негайно почала будувати інструменти навколо TLA+ і відтоді працюю в цій сфері.

Ви побудували свою кар’єру навколо формальних методів і мов програмування, від вашої ранньої роботи над інструментами на основі Temporal Logic of Actions (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 набагато більше, але те, що насправді робить його неможливим повернутися до TLA+, – це всі інструменти.

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

Найбільший зсув відбувається у змісті валідации раніше. Леслі Лемпорт, творець TLA+, порівнює написання специфікацій до коду з малюванням блупринтів до будівельних робіт. Навіть якщо ви вже побудували щось без блупрінту, все одно добре написати його зараз і використовувати його для інформування подальших змін.

У галузі програмного забезпечення ми використовуємо файли markdown та дошки. Можна порівняти це з спробою текстово описати будівлю. Це працює, але чи знаєте ви, чи сума розмірів стін додається? Quint пропонує спосіб описувати системи, де ви можете бути настільки ж високим рівнем, як хочете, і отримувати уявлення про її поведінку та правильність.

Quint будується на основі TLA+, яка широко використовується для опису розподілених систем. Як ви балансували підтримку цієї теоретичної строгості з тим, щоб зробити мову більш дружньою до розробників?

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

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

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

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

Ви також працювали над статичним аналізом та системами типів. Як ці досвіди вплинули на перевірку типів Quint, інструменти та загальний досвід розробників?

Найбільший урок, який я вивчила у цьому світі, полягає в тому, що не всі мови однакові. Ви чуєте, як люди кажуть, що це просто питання вивчення нового синтаксису, всі ті ж самі концепції все одно застосовуються, тому всі мови рівні, і це просто питання смаку. Це не правда. Область мов програмування має великих дослідників, які роблять чудову роботу для просування цієї галузі, і це не тільки для того, щоб зробити мову більш привабливою або більш до їхнього смаку.

Функціональне програмування було мені представлено дуже рано, я вивчила Haskell одночасно з C (моєю першою мовою програмування), і я дуже вдячна за це. Це основа, яка допомагає мені бачити, що ізоляція мутацій стану та невизначеності до тонкого шару в Quint, і наявність усіх складностей у чистих функціях, об’єктивно допомагає у багатьох факторах, і це не тільки питання смаку. Я не думаю, що побудова Quint була б продуктивною, якщо питання смаку були б предметом дискусії надто часто.

Викладання формальних методів як лектор дає вам унікальну перспективу. Які найбільш поширені помилкові уявлення про формальну верифікацію сьогодні?

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

Я була більш мотивована викладати їм, як формальні методи та формальна специфікація системи можуть допомогти нам розібратися у рішеннях і знайти крайні випадки, ніж зробити їх думати, що вони повинні формально верифікувати кожне програмне забезпечення, яке вони коли-небудь напишуть. Моя остаточна робота була налаштована на настільну рольову гру, де різні порядки, які гравці могли взяти, і різні налаштування мали бути враховані, намагаючись якнайбільш імітувати труднощі, з якими ми стикаємося у розподілених системах. Це виявилося досить складним, щоб вони мали використовувати інструменти для пошуку крайніх випадків і поліпшення своїх рішень для перемоги над монстрами в кінці. Надіюсь, коли вони зустрінуть подібну ситуацію на роботі колись, вони пам’ятатимуть мене. Дехто з них вже зробив це.

Є зростаючий інтерес до поєднання штучного інтелекту з розробкою програмного забезпечення. Чи бачите ви роль штучного інтелекту у допомозі розробникам писати, валідувати чи навіть генерувати формальні специфікації за допомогою інструментів, таких як Quint?

Значну, і це вже відбувається. Комп’ютерна наука більша, ніж написання коду, і штучний інтелект відкриває двері до зовсім нових способів використання формальних методів. Великі мови моделей (LLM) добре пишуть специфікації Quint з природних мовних описів системи та навіть існуючого коду. Набір LLM Quint містить агенти Claude Code, які приймають англійський опис протоколу та генерують специфікацію Quint, яку можна запустити та перевірити негайно.

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

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

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

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

З штучним інтелектом, який змінює нашу професію, принаймні до деякої міри, я сподіваюся, що цей зсув буде у бік вищого рівня проектних рішень та поведінки правильності, роблячи формальні методи щоденним інструментом; і не у бік того, щоб ми не розуміли жодного коду чи систем більше, і проводили весь наш час, переглядаючи код, згенерований штучним інтелектом, без жодного інструментарію, щоб допомогти нам розібратися в ньому.

Дякую за цікаве інтерв’ю; читачам, які цікавляться дізнатися більше про цю виконавчу мову специфікацій для моделювання та верифікації складних систем, включаючи її інструменти та те, як почати, можна ознайомитися з Quint.