Gabriela Moreira, CEO Quint v Informal Systems – rozhovor

Gabriela Moreira, CEO Quint v Informal Systems, je výzkumná inženýrka specializující se na programovací jazyky a formální metody, se silným zaměřením na vytváření nástrojů, které činí ověření složitých systémů přístupnějším inženýrům. Řídí vývoj Quintu, moderního spustitelného specifikačního jazyka založeného na TLA+, kde dále udržuje a rozvíjí jazyk a jeho nástroje. Její práce zahrnuje formální ověření, statickou analýzu a nástroje pro vývojáře, a také přispěla do akademické sféry vyučováním formálních metod, což odráží kombinaci praktického inženýrství a teoretické hloubky.

Quint, vyvinutý a udržovaný v Informal Systems, je moderní specifikační jazyk navržen pro modelování, testování a ověření složitých systémů, jako jsou distribuované sítě, blockchainy a databáze. Postavený na základech Temporal Logic of Actions (TLA), Quint představuje syntaxi bližší vývojářům, spolu s pokročilým nástrojovým vybavením, jako je typová kontrola, simulace a modelová kontrola, umožňující inženýrům detekovat systémové selhání před nasazením. Platforma zdůrazňuje spustitelné specifikace, umožňující vývojářům nejen popisovat chování systému, ale také aktivně testovat a prozkoumávat jej, mostem mezi teoretickou korektností a reálnou implementací.

Vraťme se na začátek, co vás poprvé přitáhlo k programování, a jak jste se nakonec dostala k formálním metodám a distribuovaným systémům?

Byla jsem vášnivou hráčkou s špatným počítačem, a uvědomila jsem si, že mě baví opravovat problémy a dělat ho funkčním. Zapsala jsem se na počítačovou vědu a byla jsem přitahována teorií a kompilátory. 

V roce 2015, jsem se zúčastnila programovacích soutěží. V těch, obvykle dostanete několik příkladů vstupu a očekávaného výstupu, a napíšete kód, který řeší problém a funguje pro tyto příklady. Ale poté, co jste ho odeslali k vyhodnocení, kód je vlastně testován s mnoha dalšími příklady, než ty, které vám ukázali. To uvědomění, že kód může fungovat pro scénáře, které vidím nebo si myslím, ale stále selhat v případech, které jsem neuvažovala, proměnilo programování v druh výzvy, do které jsem se zamilovala.

Pracovala jsem v průmyslu, a byla jsem rychle přitahována k distribuovaným systémům, kde jsme museli zvažovat různé pořadí, ve kterém mohou zprávy dorazit, různé režimy selhání a celý svět skrytých chování. V roce 2018, kolega mi představil formální specifikační jazyk nazvaný TLA+. Byl jsem okouzlen. Okamžitě jsem začal budovat nástroje kolem TLA+ a pracuji v tomto prostoru od té doby.

Můžete vysvětlit, co vás motivovalo soustředit se na zpřístupnění formálního ověření, a jak tato vize ovlivnila design Quintu?

TLA+ je příliš dobrý, aby nebyl široce používán v průmyslu. Byla jsem ještě bastante juniorní, když jsem se o něm dozvěděla, a účastnila jsem se těch hovorů s kolegy, abychom společně našli řešení, a neustále jsem nacházela scénáře, ve kterých naše řešení selhala. Ale byla jsem vždy poslední linií obrany proti těmto scénářům ve většině případů. Usoudila jsem, že musí existovat lepší, méně nákladný a více cenný způsob, jak tyto scénáře řešit. Takže vznikla myšlenka používat formální metody k vytvoření specifikací před implementací kódu. Proto jsem začala svou akademickou cestu tímto směrem, která mě vedla k Informal Systems a Quintu.

Quint nebyl původně koncipován jako produkt. Vyvinuli jsme ho z nutnosti v Informal Systems. Psali jsme specifikace TLA+ pro systémy, kterým jsme museli důvěřovat více, než jsme dělali, ale to se nešířilo za velmi malou skupinu lidí, protože syntaxe byla příliš děsivá s mnoha matematickými symboly, a nástrojové vybavení nevyhovovalo základním očekáváním. Ukazovali jsme kolegům a externím spolupracovníkům: „Podívejte se na tu úžasnou věc, kterou jsem udělala“, ale oni ji nemohli číst a neměli čas se naučit nový nástroj.

Designové volby v Quintu přímo následují z této zkušenosti. Jazyk je snadno čitelný a zapamatovatelný. První věc, kterou jsme postavili, byla VSCode rozšíření, které zvýrazňuje chyby, zatímco píšete. Má typy a rozdílné režimy, které explicitně oddělují vrstvy. Má REPL, abyste mohli interaktivně prozkoumávat, a simulátor, abyste mohli získat rychlou zpětnou vazbu a iterovat. Exportuje stopy do standardizovaného formátu JSON, který je snadno strojově čitelný. Tyto byly věci, které programátoři již očekávali od svých nástrojů a které jsme sami potřebovali. Ověření pod ním je stejná logika jako TLA+.

Jsem posedlá tím, aby byly formální metody více přístupné, a vydávání nástrojů je vzrušující, ale skutečný dopad je cítit pouze tehdy, když inženýrské týmy tyto nástroje skutečně používají. Stále existuje delta mezi tím, co nástroje mohou udělat, a jak užitečné se cítí pro vývojáře, a pracuji na tom, aby se tato mezera uzavřela.

Pro čtenáře, kteří nejsou s Quintem seznámeni, můžete vysvětlit, co je Quint a proč byl potřebný nový specifikační jazyk vedle existujících nástrojů, jako je TLA+?

Většina specifikací je dokumentace. Píšete, co by měl systém dělat, a kontrolujete je čtením. Problém je, že dokumentace je chybná způsoby, které mechanicky nelze detekovat: nedefinované názvy, ambivalentní chování, implicitní předpoklady. Obvykle zjistíte, zda je něco špatně, během implementace nebo v produkci.

Specifikace Quintu je něco, co můžete spustit. Modelujete systém jako stavový automat, definujete vlastnosti, které by měl splňovat, a spustíte nebo ověříte model. Pokud existuje porušení, dostanete proti-příklad ukazující přesně sekvenci kroků, které jej spustí. To mění, kdy a jak levně chytíte chybu v návrhu.

TLA+ mohl vždy dělat tohle. Quint to dělá praktickým způsobem pro inženýry, kteří nejsou již specialisté na temporální logiku.

Quint je navržen tak, aby mostem propojil formální metody a každodenní softwarové inženýrství. Jaké byly největší bariéry uživatelské přívětivosti, kterým jste se snažila zabránit ve srovnání s tradičními přístupy?

Upřímně, největší bariéra uživatelské přívětivosti byla syntaxe. To je důvod, proč jsme začali se syntaxí. Po jejím vyřešení jsme se mohli soustředit na další faktory. Systém typů a efektů Quintu přidává omezení, ale omezení, která jsou užitečná. Předcházejí celou třídu specifikačních chyb, které nejsou zábavné, když jsou nalezeny po spuštění ověření. Typy jsou téměř entirely inferovány a efekty jsou skryty před uživateli, takže přidávají hodnotu bez tření.

Největší dopad po tomto byl náš simulátor. Začal jako způsob, jak nabídnout lidem prvotní zpětnou vazbu o chování jejich systému, jako způsob, jakým vývojář chce být schopen spustit kód po jeho napsání. Ukázalo se, že je to extrémně cenné jako způsob, jak získat důvěru ve specifikace, které jsou příliš velké pro ověření, protože odbornost na přizpůsobení specifikace pro ověření by neměla být brána jako samozřejmost. Náš simulátor učinil důvěru přístupnější a my jsme ho hojně používali v mnoha projektech.

Mé největší bolesti s TLA+ syntaxí bylo, jak často jsem míchala zpětné a běžné lomítko, a musíte je psát hodně. Mám Quint syntaxi rád víc, ale co mě opravdu znepokojuje, je veškeré nástrojové vybavení.

Jedna z Quintových silných stránek je schopnost modelovat a testovat distribuované systémy před nasazením. Jak tohle mění způsob, jakým inženýři by měli uvažovat o budování systémů, jako jsou blockchainy nebo reálná infrastruktura?

Největší posun je přesunutí validace dříve. Leslie Lamport, tvůrce TLA+, porovnává psaní specifikací před kódem s kreslením modrozobrazů před stavebními pracemi. I když jste již něco postavili bez modrozobrazu, je stále dobrý nápad napsat jeden a použít ho pro informování dalších změn.

V softwarovém průmyslu používáme markdown soubory a bílé tabule. Možná můžete to porovnat s pokusem popsat budovu textově. To funguje, ale věděli byste, zda velikosti stěn souvisejí? Quint nabízí způsob, jak popsat systémy, kde můžete být tak abstraktní, jak chcete, a získat vhled do jeho chování a korektnosti.

Quint staví na základech TLA+, který je široce používán pro popis distribuovaných systémů. Jak jste vyrovnala zachování teoretické přísnosti a zároveň učinila jazyk bližším vývojářům?

Klíčovým rozhodnutím bylo omezit Quint na fragment TLA (logiky za TLA+) místo toho, aby vystavil všechno, co logika umožňuje. TLA je velmi expresivní, a část této expresivnosti zahrnuje operátory, které nejsou podporovány žádnými nástroji, a umožňuje kombinace, které lidé chápou a používají nesprávně, což činí věci opravdu těžkými na ladění. Učinili jsme úmyslné rozhodnutí: držet se toho, co většina realistických specifikací skutečně potřebuje, a vyhnout se tomu, co má potenciál pro zmatení.

Systém typů a efektů přidává omezení, ale omezení, která jsou užitečná. Předcházejí celé třídě specifikačních chyb, které nejsou zábavné, když jsou nalezeny po spuštění ověření. Typy jsou téměř entirely inferovány a efekty jsou skryty před uživateli, takže přidávají hodnotu bez tření.

Předtím, než jsem se dozvěděla o existenci TLA+, jsem dělala výzkum v oblasti typových systémů, což znamená, že typový kontrolor Quintu byl pravděpodobně mou nejoblíbenější součástí, kterou jsem napsala. Pamatuji si, že jsem pila Paçoca-flavored kávu v mých prvních měsících v Informal Systems, zatímco jsem recenzovala některé papíry o typovém systému, a myslela jsem si: „Můj život je úžasný“. 

Učinění jazyka dobrým pro použití a zároveň zachování korespondence s TLA+ (jak specifikace Quintu mohou být transpilovány do TLA+) byla cvičením v programovacím jazyce, a diskuse s týmem byly nejvíce nápomocné, následované zpětnou vazbou od raných uživatelů. Stále existují zlepšení, která chceme udělat, a možná je to moje nejoblíbenější část práce.

Můžete vysvětlit, jak vaše zkušenosti se statickou analýzou a typovými systémy ovlivnily ověření typů, nástrojové vybavení a celkovou uživatelskou zkušenost Quintu?

Největší lekce, kterou jsem se naučila v tomto světě, je, že ne všechny jazyky jsou stejné. Uslyšíte lidi, kteří říkají, že se jedná pouze o naučení nové syntaxe, všechny stejné koncepty stále platí, takže všechny jazyky jsou stejné a je to pouze otázka vkusu. To není pravda. Oblast programovacích jazyků má skvělé výzkumníky, kteří dělají úžasnou práci, aby tento obor posunuli vpřed, a to není pouze proto, aby učinili jazyk hezčím nebo bližším jejich vkusu.

Funkcionální programování mi bylo představeno velmi brzy, naučila jsem se Haskell ve stejnou dobu, jako jsem se naučila C (můj první programovací jazyk), a jsem velmi vděčná za to. To je základ, který mi pomáhá vidět, že izolování stavových mutací a nedeterminismu do tenké vrstvy v Quintu a mít veškerou složitost v čistých funkcích objektivně pomáhá ve mnoha faktorech, a není to pouze otázka vkusu. Nemyslím si, že by bylo produktivní budovat Quint, kdyby byly otázky vkusu často diskutovány.

Jako lektor, který učí formální metody, máte jedinečný pohled. Jaké jsou nejčastější mýty, které inženýři mají o formálním ověření dnes?

Nu, učila jsem studenty, kteří byli teprve na počátku své kariéry v průmyslu. Velká většina z nich nikdy předtím neslyšela o formálních metodách nebo formálním ověření, takže žádné mýty! Kurikulum bylo vytvořeno tak, aby většina z nich se také nedozvěděla o distribuovaných systémech, a asi polovina z nich se dozvěděla o vláknech ve stejném semestru. Říkala jsem jim, že se cítím, jako bych učila, co je deštník dobrý, předtím, než zažili déšť!

Byla jsem více motivována učit je, jak formální metody a formální specifikace systému mohou pomoci nám uvažovat o řešeních a najít hraniční případy, než je přesvědčovat, aby formálně ověřovali každý software, který kdy napíšou. Moje závěrečná práce byla nastavení stolní RPG, kde různé objednávky, které hráči mohli vzít, a různé nastavení musely být vzaty v úvahu, snažící se napodobit obtíže, kterým čelíme v distribuovaných systémech, tolik, kolik to bylo možné. To se podařilo být dostatečně těžké, aby museli použít nástroje, aby našli hraniční případy a zlepšili svá řešení pro poražení monster na konci. Doufám, že když budou jednou v práci čelit podobné situaci, budou si mě pamatovat. Některé z nich už to udělaly.

Existuje rostoucí zájem o kombinování AI se softwarovým vývojem. Vidíte roli pro AI v pomoci vývojářům psát, ověřovat nebo dokonce generovat formální specifikace pomocí nástrojů, jako je Quint?

Značnou roli, a již se to děje. Computer Science je větší než psaní kódu, a AI otevírá dveře úplně novým způsobům, jak používat formální metody. LLM jsou dobré v psaní specifikací Quint z popisů systému v přirozeném jazyce a dokonce i existujícím kódem. Kit LLM Quint má agenty Claude Code, kteří berou anglický popis protokolu a produkují specifikaci Quint, kterou můžete spustit a zkontrolovat okamžitě.

Současně Quint také pomáhá vývojářům důvěřovat kódu napsanému s AI. Silně věřím, že důvěra musí pocházet z porozumění, ne z nějakých magických zaškrtnutí. Práce na specifikaci Quintu, která řídí a kontroluje implementační kód, znamená, že vývojáři mohou stále vlastnit a chápat chování systému, řeší kognitivní dluh, který může použití AI vytvořit, a poskytuje více asertivní způsoby ověření generovaného kódu.

Využíváme LLM jako jazykové nástroje, které píší přesné definice Quint z přirozeného jazykového záměru, a pak dáváme Quint nástrojům AI, aby mohli dělat věci, které nemohou spolehlivě udělat sami, jako najít hraniční případy.

Pohledem do budoucna, co se musí stát, aby se formální metody staly standardní součástí softwarového vývojového cyklu?

Po nějakou dobu již vím, že dvě hlavní věci, které Quint potřebuje pro větší přijetí: nižší náklady a vyšší hodnota. Myslím, že to platí i pro mnoho dalších věcí. Formální metody právě získaly velký impuls v obou těchto věcech, s AI značně snižujícím náklady na psaní formálních specifikací a zároveň vytvářejícím prostředí nedůvěry a nepochopení, kde formální metody mohou být nejvíce účinné a cenné.

S AI měnícím, co je naše profese, alespoň do jisté míry, doufám, že tato změna směřuje k vyššímu designu a chování korektnosti, dělající formální metody každodenním nástrojem; a ne k tomu, aby jsme nerozuměli žádnému kódu nebo systémům již, a trávili veškerý čas recenzí kódu generovaného AI bez žádného nástroje, který by nám pomáhal rozumět jim.

Děkuji za vhledný rozhovor; čtenáři, kteří se chtějí dozvědět více o tomto spustitelném specifikačním jazyku pro modelování a ověřování složitých systémů, včetně jeho nástrojového vybavení a toho, jak se s ním začít, mohou prozkoumat Quint.