Gabriela Moreira, VD för Quint på Informal Systems – Intervjuserie

Gabriela Moreira, VD för Quint på Informal Systems, är en forskningsingenjör som specialiserat sig på programmeringsspråk och formella metoder, med ett starkt fokus på att bygga verktyg som gör komplex systemverifiering mer tillgänglig för ingenjörer. Hon leder utvecklingen av Quint, ett modernt specifikationsspråk baserat på TLA+, där hon fortsätter att underhålla och utveckla språket och dess verktyg. Hennes arbete omfattar formell verifiering, statisk analys och utvecklarverktyg, och hon har också bidragit till akademin genom att undervisa i formella metoder, vilket visar en blandning av praktisk ingenjörskap och teoretisk djup.

Quint, som utvecklas och underhålls av Informal Systems, är ett modernt specifikationsspråk som är utformat för att modellera, testa och verifiera komplexa system som distribuerade nätverk, blockkedjor och databaser. Byggt på grunderna av Temporal Logic of Actions (TLA), introducerar Quint en mer utvecklarvänlig syntax, tillsammans med avancerad verktygsutveckling som typkontroll, simulering och modellkontroll, som gör det möjligt för ingenjörer att upptäcka systemsfel innan distribution. Plattformen betonar exekverbara specifikationer, vilket möjliggör för utvecklare att inte bara beskriva systembeteende utan också aktivt testa och utforska det, och därmed överbrygga gapet mellan teoretisk korrekthet och verklig implementering.

Om vi går tillbaka till början, vad var det som först väckte ditt intresse för programmering, och hur hamnade du till slut inom formella metoder och distribuerade system?

Jag var en ivrig spelare med en dålig dator, och jag insåg att jag njöt av att lösa problemen och få det att fungera. Jag anmälde mig till datavetenskap och drogs till teori och kompilatorer. 

2015 presenterades jag för programmeringstävlingar. Där får man vanligtvis några exempel på indata och förväntad utdata, och man skriver kod som löser problemet och fungerar för de exempel man ser. Men efter att man har skickat in koden för utvärdering testas den faktiskt med många fler exempel än de man visar. Den insikten att koden kanske fungerar för de scenarier jag ser eller tänker på, men fortfarande kan misslyckas i fall jag inte har övervägt, gjorde programmering till en sorts utmaning som jag blev kär i.

När jag arbetade i branschen drogs jag snabbt till distribuerade system, där vi måste överväga olika ordningar som meddelanden kan anlända i, olika felmoder och en hel värld av dolda beteenden. 2018 introducerade en kollega mig till ett formellt specifikationsspråk som kallades TLA+. Jag var fast. Jag började omedelbart bygga verktyg kring TLA+ och har arbetat i det här området sedan dess.

Du har byggt din karriär kring formella metoder och programmeringsspråk, från ditt tidiga arbete med verktyg baserade på Temporal Logic of Actions (TLA+) till att leda utvecklingen av Quint på Informal Systems. Vad motiverade dig att fokusera på att göra formell verifiering mer tillgänglig, och hur har den visionen format Quints design?

TLA+ är för bra för att inte användas omfattande i branschen. Jag var fortfarande ganska junior när jag lärde mig om det, och jag deltog i samtal med mina arbetskamrater för att försöka komma på lösningar tillsammans, och jag upptäckte ständigt scenarier där våra lösningar skulle misslyckas. Men jag var alltid den sista försvarslinjen mot dessa scenarier i de flesta fall. Jag insåg att det måste finnas ett bättre, mindre kostsamt och mer värdefullt sätt att lösa dessa scenarier på. Så jag började min akademiska resa mot det, vilket ledde mig till Informal Systems och Quint.

Quint var inte ursprungligen tänkt som en produkt. Vi byggde det av nödvändighet på Informal Systems. Vi skrev TLA+-specifikationer för system som vi behövde lita på mer än vi gjorde, men som inte expanderade bortom en mycket liten grupp människor eftersom syntaxen var för skrämmande med för många matematiska symboler, och verktygen motsvarade inte människors grundläggande förväntningar. Vi visade kollegor och externa samarbetspartner: “se på den här fantastiska saken jag gjorde”, men de kunde inte läsa den, och hade inte tid att lära sig ett nytt verktyg.

Designvalen i Quint följer direkt från den erfarenheten. Språket är lätt att läsa och komma ihåg. Det första vi byggde var en VSCode-tillägg som markerar fel när man skriver. Det har typer och distinkta lägen för att separera lager explicit. Det har en REPL så att man kan utforska interaktivt, och en simulator så att man kan få snabb återkoppling och iterera. Det exporterar spår till ett standardiserat JSON-format som är lätt för maskiner att tolka. Detta var saker som programmerare redan förväntade sig av sina verktyg och som vi själva behövde. Den underliggande verifieringen är samma logik som TLA+.

Jag är besatt av att göra formella metoder mer tillgängliga, och att leverera verktyg är spännande, men den verkliga påverkan upplevs bara om ingenjörsteam faktiskt använder dem. Det finns fortfarande en skillnad mellan vad verktygen kan göra och hur användbara de känns för utvecklare, och jag arbetar för att stänga den gapet.

För läsare som inte är bekanta med det, hur skulle du förklara vad Quint är och varför ett nytt specifikationsspråk behövdes bredvid befintliga verktyg som TLA+?

De flesta specifikationer är dokumentation. Man skriver ner vad systemet ska göra, och man kontrollerar dem genom att läsa dem. Problemet är att dokumentation kan vara fel på sätt som inte kan upptäckas mekaniskt: odefinierade namn, tvetydigt beteende, implicita antaganden. Man upptäcker vanligtvis det under implementeringen eller i produktionen.

En Quint-specifikation är något man kan exekvera. Man modellerar systemet som en tillståndsmaskin, definierar egenskaperna det ska uppfylla, och kör eller verifierar modellen. Om det finns en överträdelse, får man ett motexempel som visar exakt den sekvens av steg som utlöser det. Det förändrar när och hur billigt man upptäcker en designfel.

TLA+ kunde alltid göra detta. Quint gör det praktiskt för ingenjörer som inte redan är specialister inom temporal logik.

Quint är utformat för att överbrygga gapet mellan formella metoder och vardaglig programvaruutveckling. Vilka var de största användbarhetsbarriärerna du syftade till att eliminera jämfört med traditionella tillvägagångssätt?

Ärligt talat var den största användbarhetsbarriären syntaxen. Det är därför vi började med syntaxen. Efter att ha hanterat det kunde vi fokusera mer på andra faktorer. Quints typ- och effektsystem kom för att flagga så många fel som möjligt innan den vanliga verifieringsprocessen ens började, och människor uppskattade det mycket. Det ledde oss att skriva högkvalitativa specifikationer som ännu fler kunde läsa. Vi integrerade allt i redigerare och erbjöd den grundläggande funktionaliteten som alla utvecklare har rätt att förvänta sig.

Den största påverkan efter det var vår simulator. Den började som ett sätt att erbjuda människor första återkopplingen om systemets beteende, som en utvecklare vill kunna “köra koden” efter att ha skrivit den. Det visade sig sedan vara extremt värdefullt som ett sätt att få förtroende för specifikationer som är för stora för att verifieringen ska kunna hantera, eftersom expertisen att anpassa en specifikation för att göra den möjlig för verifiering inte ska tas för givet. Vår simulator gjorde förtroendet mer tillgängligt och vi har använt den omfattande i många projekt.

Mitt största smärtproblem med TLA+-syntaxen var hur ofta jag blandade mina snedstreck och vanliga snedstreck, och man måste skriva många av dem. Jag gillar Quints syntax mycket bättre, men det som verkligen gör det omöjligt för mig att gå tillbaka är alla verktygen.

En av Quints styrkor är dess förmåga att modellera och testa distribuerade system innan distribution. Hur förändrar detta sättet ingenjörer bör tänka på att bygga system som blockkedjor eller realtidsinfrastruktur?

Den största förändringen är att flytta valideringen tidigare. Leslie Lamport, skaparen av TLA+, jämför skrivande av specifikationer före kod med att rita blåkopior före byggnadsarbeten. Även om man redan har byggt något utan en blåkopia, är det fortfarande en bra idé att skriva en nu och använda den för att informera om framtida ändringar.

I programvaruindustrin använder vi markdown-filer och whiteboards. Kanske kan man jämföra det med att försöka beskriva en byggnad textuellt. Det fungerar, men skulle man veta om väggstorlekarna adderar upp? Quint erbjuder ett sätt att beskriva system där man kan vara så högnivå som man vill, och få insikter om dess beteende och korrekthet.

Quint bygger på grunderna av TLA+, som är allmänt använd för att beskriva distribuerade system. Hur balanserade du behovet av att upprätthålla den teoretiska rigorositeten medan du gjorde språket mer utvecklarvänligt?

Den avgörande beslutet var att begränsa Quint till en delmängd av TLA (logiken bakom TLA+) snarare än att exponera allt som logiken tillåter. TLA är mycket uttrycksfullt, och en del av den uttrycksfullheten inkluderar operatorer som inte stöds av några verktyg, och tillåter kombinationer som människor förstår och använder felaktigt, vilket gör det mycket svårt att felsöka. Vi gjorde ett medvetet val: håll fast vid vad de flesta realistiska specifikationer faktiskt behöver, och undvik det som har potential för förvirring.

Typsystemet och effektsystemet lägger till begränsningar, men begränsningar som är användbara. De förhindrar en hel klass av specifikationsfel som inte är roliga när de upptäcks efter att verifieringen redan har startat. Typer är nästan helt infärda och effekter är dolda för användarna, så detta lägger till värde utan någon friktion.

Innan jag lärde mig om TLA+:s existens, gjorde jag forskningsarbete i typsystem, vilket betyder att Quints typkontroll var troligen min favoritkomponent att skriva. Jag minns att jag drack en Paçoca-smakande kaffe under mina första månader på Informal medan jag granskade en typsystemartikel och tänkte “mitt liv är underbart”. 

Att göra språket bra att använda samtidigt som man behåller korrespondensen med TLA+ (då Quint-specifikationer kan konverteras till TLA+) var ett programmeringsspråksövning, och diskussioner med teamet var den mest hjälpsamma resursen, följt av feedback från tidiga användare. Det finns fortfarande förbättringar vi vill göra, och det kan vara min favoritdel av jobbet.

Du har också arbetat med statisk analys och typsystem. Hur har dessa erfarenheter påverkat Quints typkontroll, verktyg och övergripande utvecklarupplevelse?

Den största lärdomen jag lärde mig i den världen är att inte alla språk är desamma. Man hör människor säga att det bara handlar om att lära sig en ny syntax, alla samma koncept gäller fortfarande, så alla språk är lika och det är bara en fråga om smak. Det är inte sant. Området programmeringsspråk har stora forskare som gör fantastiskt arbete för att främja detta område, och det är inte bara för att göra ett språk se bättre ut eller mer till deras smak.

Funktionell programmering introducerades för mig mycket tidigt, jag lärde mig Haskell samtidigt som jag lärde mig C (mitt första programmeringsspråk), och jag är mycket tacksam för det. Detta är grunden som hjälper mig att se att isolering av tillståndsändringar och icke-determinism till ett tunt lager i Quint, och ha all komplexitet i ren funktion, objektivt hjälper till i många faktorer, och det är inte bara en fråga om smak. Jag tror inte att byggandet av Quint skulle ha varit produktivt om smaksaker var upp till diskussion alltför ofta.

Som lärare i formella metoder ger dig en unik perspektiv. Vilka är de vanligaste missuppfattningarna som ingenjörer har om formell verifiering idag?

Jag undervisade studenter som precis började i branschen. Den överväldigande majoriteten av dem hade aldrig hört talas om formella metoder eller formell verifiering tidigare, så inga missuppfattningar! Läroplanen var utformad så att de flesta av dem inte heller lärde sig om distribuerade system, och ungefär hälften av dem skulle lära sig om trådar under samma termin. Jag sa till dem att jag kände att jag lärde dem vad en paraply är bra för innan de hade upplevt någon regn!

Jag var mer motiverad att lära dem hur formella metoder och formellt specificerande av ett system kan hjälpa oss att resonera om lösningar och hitta kanterfall, snarare än att göra dem tro att de ska formellt verifiera all programvara de någonsin skriver. Min slutuppgift var en bordsspelets uppställning där olika ordningar som spelare kunde ta och olika uppställningar måste beaktas, och försöka efterlikna svårigheterna vi möter i distribuerade system så mycket som möjligt. Det lyckades med att vara tillräckligt svårt så att de måste använda verktygen för att hitta kanterfall och förbättra sina lösningar för att besegra monstren i slutet. Förhoppningsvis kommer de att komma ihåg mig när de möter en liknande situation på jobbet en dag. Några av dem har redan gjort det.

Det finns ett växande intresse för att kombinera AI med programvaruutveckling. Ser du en roll för AI i att hjälpa utvecklare att skriva, validera eller till och med generera formella specifikationer med hjälp av verktyg som Quint?

En betydande roll, och det händer redan. Datavetenskap är större än att skriva kod, och AI öppnar dörren till helt nya sätt att använda formella metoder. LLM:er är bra på att skriva Quint-specifikationer från naturligt språkbeskrivningar av ett system och till och med befintlig kod. Quint LLM Kit har Claude Code-agenter som tar en engelsk beskrivning av ett protokoll och producerar en Quint-specifikation som man kan köra och kontrollera omedelbart.

Samtidigt hjälper Quint också utvecklare att lita på kod skriven med AI. Jag tror starkt på att förtroendet måste komma från förståelse, inte några magiska checkmarkeringar. Att arbeta med en Quint-specifikation som driver och kontrollerar implementeringskoden betyder att utvecklare fortfarande kan äga och förstå systemets beteende, och hantera den kognitiva skulden som AI-användning kan skapa, och ge mer pålitliga sätt att validera den genererade koden.

Vi använder LLM:er som språkverktyg som skriver Quint-precisa definitioner från naturligt språkavsett, och sedan ger Quint-verktygen till AI så att det kan åstadkomma saker som det inte kan göra på ett tillförlitligt sätt på egen hand, som att hitta kanterfall.

Om vi ser framåt, vad behöver hända för att formella metoder ska gå från nischad användning till en standarddel av programvaruutvecklingslivscykeln?

För en tid sedan visste jag att de två övergripande sakerna Quint behöver för mer antagande: lägre kostnad och högre värde. Jag tror att detta gäller för många andra saker också. Formella metoder fick just en stor boost i båda dessa saker, med AI som kraftigt minskar kostnaden för att skriva formella specifikationer och också skapar en miljö av bristande tillit och förståelse där formella metoder kan vara som mest påverkande och värdefulla.

Med AI som förändrar vad vår profession är, åtminstone till viss del, hoppas jag att denna förändring är mot högnivådesignbeslut och beteendekorrekthet, och gör formella metoder till ett vardagligt verktyg; och inte mot att vi inte förstår någon kod eller system längre och tillbringar all vår tid med att granska AI-genererad kod utan något verktyg för att hjälpa oss att resonera om det.

Tack för den insiktsfulla intervjun; läsare som är intresserade av att lära sig mer om detta exekverbara specifikationsspråk för modellering och verifiering av komplexa system, inklusive dess verktyg och hur man kommer igång, kan utforska Quint.