Gabriela Moreira, CEO av Quint i Informal Systems – Intervju-serie

Gabriela Moreira, CEO av Quint i Informal Systems, er en forskningsingeniør som spesialiserer seg på programmeringsspråk og formelle metoder, med sterkt fokus på å bygge verktøy som gjør kompleks systemverifisering mer tilgjengelig for ingeniører. Hun leder utviklingen av Quint, et moderne eksekverbart spesifikasjonsspråk basert på TLA+, hvor hun fortsatt vedlikeholder og utvikler språket og dens verktøy. Hennes arbeid omfatter formell verifisering, statisk analyse og utviklerverktøy, og hun har også bidratt til akademia ved å undervise i formelle metoder, noe som reflekterer en blanding av praktisk ingeniørarbeid og teoretisk dybde.

Quint, utviklet og vedlikeholdt av Informal Systems, er et moderne spesifikasjonsspråk designet for å modellere, teste og verifisere komplekse systemer som distribuerte nettverk, blokkjeder og databaser. Bygget på grunnlag av Temporal Logic of Actions (TLA), introduserer Quint en mer utviklervennlig syntaks, sammen med avansert verktøy som typekontroll, simulering og modellkontroll, som gjør det mulig for ingeniører å oppdage systemfeil før distribusjon. Plattformen legger vekt på eksekverbare spesifikasjoner, som gjør det mulig for utviklere å ikke bare beskrive systematferd, men også aktivt teste og utforske det, og å lukke gapet mellom teoretisk korrekthet og virkelig implementering.

Tilbake til begynnelsen, hva var det som først vekket din interesse for programmering, og hvordan kom du til å arbeide med formelle metoder og distribuerte systemer?

Jeg var en ivrig gamer med en dårlig datamaskin, og jeg innser at jeg likte å fikse problemene og gjøre det fungere. Jeg meldte meg på computer vitenskap og ble trukket mot teori og kompilatorer. 

I 2015, ble jeg presentert for programmeringskonkurranser. I disse, får du vanligvis noen eksempler på inn- og forventet ut-data, og du skriver kode som løser problemet og fungerer for disse eksemplene. Men etter at du har levert det for evaluering, blir koden faktisk testet med mange flere eksempler enn de som vises deg. Denne realiseringen om at kode kan fungere for scenariene jeg ser eller tenker på, men likevel feile i tilfeller jeg ikke har vurdert, gjorde programmering til en slags utfordring jeg ble forelsket i.

Når jeg arbeidet i industrien, ble jeg raskt trukket mot distribuerte systemer, hvor vi måtte vurdere forskjellige rekkefølger meldinger kunne ankomme i, forskjellige feilmodi og en hel verden av skjulte atferd. I 2018, introduserte en kollega meg for et formelt spesifikasjonsspråk kalt TLA+. Jeg ble fanget. Jeg startet umiddelbart å bygge verktøy rundt TLA+ og har arbeidet i dette området siden.

Du har bygget din karriere rundt formelle metoder og programmeringsspråk, fra ditt tidlige arbeid med verktøy basert på Temporal Logic of Actions (TLA+) til å lede utviklingen av Quint i Informal Systems. Hva motiverte deg til å fokusere på å gjøre formell verifisering mer tilgjengelig, og hvordan har den visjonen formet Quints design?

TLA+ er for godt ikke å bli brukt omfattende i industrien. Jeg var fortsatt ganske junior da jeg lærte om det, og jeg ville delta i samtaler med mine arbeidskolleger for å prøve å finne løsninger sammen, og jeg var alltid den siste forsvarslinjen mot disse scenariene i de fleste tilfeller. Jeg fant ut at det måtte finnes en bedre, mindre kostbar og mer verdifull måte å løse disse scenariene på. Så jeg startet min akademiske reise mot det, som ledet meg til Informal Systems og Quint.

Quint var ikke opprinnelig tenkt som et produkt. Vi bygde det av nødvendighet i Informal Systems. Vi skrev TLA+-spesifikasjoner for systemer vi trengte å stole på mer enn vi gjorde, men det utvidet seg ikke utenfor en svært liten gruppe mennesker, da syntaksen var for skremmende med for mange matematiske symboler, og verktøyet møtte ikke folks grunnleggende forventninger. Vi viste kolleger og eksterne samarbeidspartnere: “se på denne fantastiske ting jeg gjorde”, men de kunne ikke lese det, og hadde ikke tid til å lære et nytt verktøy.

Designvalgene i Quint følger direkte fra den erfaringen. Språket er lett å lese og huske. Det første vi bygde, var en VSCode-utvidelse som høydepunkter feil mens du skriver. Det har typer og distinkte moduser for å skille lag eksplisitt. Det har en REPL, så du kan utforske interaktivt, og en simulator, så du kan få rask tilbakemelding og iterere. Det eksporterer spor til en standardisert JSON-format som er lett for maskiner å parse. Disse var ting programmerere allerede forventet av sine verktøy og som vi selv trengte. Verifiseringen under er den samme logikken som TLA+.

Jeg er besatt av å gjøre formelle metoder mer tilgjengelige, og å levere verktøy er spennende, men den virkelige impakten føles bare hvis ingeniørteam faktisk bruker dem. Det er fortsatt en delta mellom hva verktøyene kan gjøre og hvor nyttige de føles for utviklere, og jeg arbeider for å lukke den gapen.

For lesere som ikke er kjent med det, hvordan ville du forklare hva Quint er og hvorfor et nytt spesifikasjonsspråk var nødvendig sammen med eksisterende verktøy som TLA+?

De fleste spesifikasjoner er dokumentasjon. Du skriver ned hva systemet skal gjøre, og du sjekker dem ved å lese dem. Problemet er at dokumentasjon er feil på måter du ikke mekanisk kan oppdage: udefinerte navn, tvetydig atferd, implisitte antagelser. Du oppdager vanligvis ut under implementering eller i produksjon.

En Quint-spesifikasjon er noe du kjører. Du modellerer systemet som en tilstandsmaskin, definerer egenskapene det skal oppfylle, og kjører eller verifiserer modellen. Hvis det er en overtredelse, får du en moteksempel som viser nøyaktig sekvensen av steg som utløser det. Det endrer når og hvor billig du fanger en designfeil.

TLA+ kunne alltid gjøre dette. Quint gjør det praktisk for ingeniører som ikke allerede er spesialister i temporal logikk.

Quint er designet for å lukke gapet mellom formelle metoder og hverdagslig programvareutvikling. Hva var de største brukervennlighetsbarrierene du forsøkte å eliminere i forhold til tradisjonelle tilnærminger?

Ærlig talt, den største brukervennlighetsbarrieren var syntaksen. Det er derfor vi startet med syntaksen. Etter å ha adressert det, kunne vi fokusere mer på andre faktorer. Quints type- og effektsystem kom for å flagge så mange feil som mulig før selv den vanlige verifiseringsprosessen startet, og folk verdsatte det mye. Det ledet oss til å skrive mer kvalitetsfulle spesifikasjoner som enda flere mennesker kunne lese. Vi integrerte det alt i redaktorer og tilbød den grunnleggende funksjonaliteten alle utviklere har rett til å forvente.

Den største impakten etter det var vår simulator. Den startet som bare en måte å tilby mennesker første tilbakemelding på systemets atferd, som en utvikler ønsker å kunne, noenlunde, kjøre koden etter å ha skrevet den. Det viste seg å være ekstremt verdifullt som en måte å få tillit til spesifikasjoner som er for store for verifisering å håndtere, siden ekspertisen i å tilpasse en spesifikasjon for å gjøre den mulig for verifisering, bør ikke tas for gitt. Vår simulator gjorde tillit mer tilgjengelig, og vi har brukt det omfattende i mange prosjekter.

Min største smerte med TLA+-syntaksen var hvor ofte jeg blandet sammen min bakslashes og vanlige slashes, og du må skrive disse tegnene mye. Jeg liker Quints syntaks mye bedre, men det som virkelig gjør det umulig å gå tilbake for meg, er all verktøyingen.

En av Quints styrker er evnen til å modellere og teste distribuerte systemer før distribusjon. Hvordan endrer dette måten ingeniører bør tenke om å bygge systemer som blokkjeder eller sanntids-infrastruktur?

Den største skiftet er å flytte validering tidligere. Leslie Lamport, skaperen av TLA+, sammenligner å skrive spesifikasjoner før kode med å tegne blåkopier før byggingen starter. Selv om du allerede har bygget noe uten en blåkopi, er det fortsatt en god idé å skrive en nå og bruke den til å informere dine videre endringer.

I programvareindustrien, bruker vi markdown-filer og whiteboards. Kanskje kan du sammenligne det med å forsøke å tekstlig beskrive et bygg. Det fungerer, men ville du vite om veggstørrelsene summerer seg opp? Quint tilbyr en måte å beskrive systemer hvor du kan være så høyt nivå som du ønsker, og få innsikt i dens atferd og korrekthet.

Quint bygger på grunnlag av TLA+, som er vidt brukt til å beskrive distribuerte systemer. Hvordan balanserte du vedlikehold av den teoretiske styrken mens du gjorde språket mer utviklervennlig?

Den avgjørende beslutningen var å begrense Quint til en delmengde av TLA (logikken bak TLA+) snarere enn å eksponere alt logikken tillater. TLA er svært uttrykksfullt, og noen av den uttrykksfulle inkluderer operatorene som ikke støttes av noen verktøy, og tillater kombinasjoner som mennesker forstår og bruker feil, og gjør det virkelig vanskelig å feilsøke. Vi tok en bevisst beslutning: stikk til det som de fleste realistiske spesifikasjoner faktisk trenger, og unngå det som har potensial for forvirring.

Type-systemet og effekt-systemet legger til begrensninger, men begrensninger som er nyttige. De forhindrer en hel klasse av spesifikasjonsfeil som ikke er morsomme når de oppdages etter at verifiseringen allerede har startet. Typer er nesten helt inferert, og effekter er skjult for brukerne, så dette legger til verdi uten friksjon.

Før jeg lærte om TLA+’s eksistens, gjorde jeg forskningsarbeid i type-systemer, som betyr at Quints typekontroll var kanskje min favorittkomponent å skrive. Jeg husker å drikke en Paçoca-smak kaffe i mine første måneder hos Informal Systems, mens jeg gjennomgikk en type-system papir og tenkte “mitt liv er fantastisk”. 

Å gjøre språket bra å bruke, samtidig som det fortsatt korresponderer med TLA+ (siden Quint-spesifikasjoner kan konverteres til TLA+), var et programmeringsspråk-øvelse, og diskusjoner med teamet var den mest nyttige ressursen, fulgt av tilbakemelding fra tidlige brukere. Det er fortsatt forbedringer vi ønsker å gjøre, og det kan være min favoritt-del av jobben.

Du har også arbeidet med statisk analyse og type-systemer. Hvordan har disse erfaringene påvirket Quints typekontroll, verktøy og generell utvikleropplevelse?

Den største lærdommen jeg lærte i den verden, er at ikke alle språk er like. Du hører folk si at det bare er en måte å lære en ny syntaks, alle samme konseptene gjelder fortsatt, så alle språk er like og det er bare en måte å lære det på. Det er ikke sant. Feltet programmeringsspråk har store forskere som gjør fantastisk arbeid for å fremme dette feltet, og det er ikke bare for å gjøre et språk se penere ut eller mer til deres likning.

Funksjonell programmering ble introdusert for meg svært tidlig, jeg lærte Haskell samtidig som jeg lærte C (mitt første programmeringsspråk), og jeg er svært takknemlig for det. Dette er grunnlaget som hjelper meg å se at isolering av stat-mutasjoner og ikke-determinisme til et tynt lag i Quint, og å ha all kompleksitet i rene funksjoner, objektivt hjelper på mange faktorer, og det er ikke bare en måte å gjøre det på. Jeg tror ikke bygging av Quint ville ha vært produktivt hvis saker som smak var oppe til diskusjon ofte.

Undervisning i formelle metoder som foreleser gir deg en unik perspektiv. Hva er de mest vanlige misforståttene ingeniører har om formell verifisering i dag?

Vel, jeg underviste studenter som bare var i gang med å komme inn i industrien. Det aller meste av dem hadde aldri hørt om formelle metoder eller formell verifisering før, så ingen misforståttelse! Kurset var lagt slik at de fleste av dem heller ikke lærte om distribuerte systemer, og om halvparten av dem ville lære om tråder i samme semester. Jeg sa til dem at jeg følte meg som om jeg underviste dem i hva en paraply er god for før de hadde opplevd noen regn!

Jeg var mer motivert til å undervise dem i hvordan formelle metoder og å spesifisere et system formelt kan hjelpe oss å granske løsninger og finne kanter, enn å få dem til å tro at de burde formelt verifisere all programvare de noen gang skrev. Min siste oppgave var en bord-rollespill-oppsetting hvor forskjellige rekkefølger spillere kunne ta og forskjellige oppsett måtte tas i betraktning, og prøve å etterligne vanskelighetene vi møter i distribuerte systemer så mye som mulig. Det lyktes i å være hardt nok at de måtte bruke verktøyene til å finne kanter og forbedre løsningene for å slå monsterne til slutt. Jeg håper at når de møter en lignende situasjon på jobben en dag, vil de huske meg. Noen av dem har allerede gjort det.

Det er en økende interesse for å kombinere AI med programvareutvikling. Ser du en rolle for AI i å hjelpe utviklere å skrive, validere eller selv generere formelle spesifikasjoner med verktøy som Quint?

En betydelig en, og det skjer allerede. Informatikk er større enn å skrive kode, og AI åpner døren til helt nye måter å bruke formelle metoder på. LLM-er er gode til å skrive Quint-spesifikasjoner fra naturlige språkbeskrivelser av et system og selv eksisterende kode. Quint LLM Kit har Claude Code-agenter som tar en engelsk beskrivelse av en protokoll og produserer en Quint-spesifikasjon du kan kjøre og sjekke umiddelbart.

Samtidig hjelper Quint også utviklere å stole på kode skrevet med AI. Jeg tror sterkt på at tillit må komme fra forståelse, ikke noen magiske merk. Å arbeide med en Quint-spesifikasjon som driver og sjekker implementeringskoden, betyr at utviklere fortsatt kan eie og forstå atferden til systemet, og løse den kognitive gjelden som AI-bruk kan skape, og gi mer assertive måter å validere den genererte koden på.

Vi utnytter LLM-er som språkverktøy som skriver Quint-presise definisjoner fra det naturlige språk-intent, og så gir Quint-verktøyene til AI, så den kan utføre ting den ikke kan gjøre på egen hånd, som å finne kanter.

Ser fremover, hva må skje for at formelle metoder skal gå fra nisje-tilpasning til en standard del av programvareutviklingslivssyklusen?

For en stund nå, vet jeg de to høynivå-tingene Quint trenger for mer tilpasning: lavere kostnad og høyere verdi. Jeg tror dette gjelder for mange andre ting også. Formelle metoder fikk nylig en stor boost i både disse tingene, med AI som betydelig reduserte kostnaden av å skrive formelle spesifikasjoner og også skapte en miljø av mangel på tillit og forståelse hvor formelle metoder kan være mest effektive og verdifulle.

Med AI som endrer hva vår profesjon er, i alle fall til en viss grad, håper jeg at denne endringen går mot høyere-nivå-designvalg og atferdskorrekthet, og gjør formelle metoder til en hverdagsverktøy; og ikke mot at vi ikke forstår noen kode eller systemer lenger, og tilbringer all vår tid på å gjennomgå AI-generert kode uten noen verktøy til å hjelpe oss å granske det.

Takk for det innledende intervjuet; lesere som er interessert i å lære mer om dette eksekverbare spesifikasjonsspråket for å modellere og verifisere komplekse systemer, inkludert dens verktøy og hvordan du kommer i gang, kan utforske Quint.