Gabriela Moreira, CEO of Quint at Informal Systems – Interview Series

Gabriela Moreira, CEO of Quint at Informal Systems, er en forskningsingeniør, der specialiserer sig i programmeringssprog og formelle metoder, med stærkt fokus på at bygge værktøjer, der gør kompleks systemverificering mere tilgængelig for ingeniører. Hun står i spidsen for udviklingen af Quint, et moderne eksekverbart specifikationssprog baseret på TLA+, hvor hun fortsat vedligeholder og udvikler sproget og dets værktøjer. Hendes arbejde omfatter formel verificering, statisk analyse og udviklerværktøjer, og hun har også bidraget til akademiet ved at undervise i formelle metoder, hvilket afspejler en blanding af praktisk ingeniørarbejde og teoretisk dybde.

Quint, der er udviklet og vedligeholdt af Informal Systems, er et moderne specifikationssprog designed til at modelere, teste og verificere komplekse systemer som f.eks. distribuerede netværk, blockchains og databaser. Bygget på grundlag af Temporal Logic of Actions (TLA), introducerer Quint en mere udviklervenlig syntaks samt avanceret værktøjer som typekontrol, simulation og modelkontrol, der giver ingeniører mulighed for at opdage systemfejl før implementering. Platformen lægger vægt på eksekverbare specifikationer, der giver udviklere mulighed for ikke kun at beskrive systemadfærd, men også aktivt at teste og udforske den, og derved lukke gapet mellem teoretisk korrekthed og virkelighedsimplementering.

Tilbage til begyndelsen, hvad var det, der først vækkede din interesse for programmering, og hvordan fandt du vej ind i formelle metoder og distribuerede systemer?

Jeg var en ivrig gamer med en dårlig computer, og jeg fik indsigt i, at jeg nød at løse problemerne og få det til at virke. Jeg tilmeldte mig computervidenskab og blev tiltrukket af teori og compiler.

I 2015 blev jeg præsenteret for programmeringskonkurrencer. I disse konkurrencer får du normalt nogle eksempler på input og forventet output, og du skriver kode, der løser problemet og fungerer for de eksempler, du ser. Men efter at du har indsendt det til evaluering, testes koden faktisk med mange flere eksempler end dem, de viser dig. Den indsigt, at koden måske fungerer for de scenarier, jeg ser eller tænker på, men stadig kan fejle i tilfælde, jeg ikke har overvejet, gjorde programmering til en slags udfordring, jeg blev forelsket i.

Da jeg arbejdede i industrien, blev jeg hurtigt tiltrukket af distribuerede systemer, hvor vi skulle overveje forskellige ordninger af beskeder, der kunne ankomme, forskellige fejltilstande og en hel verden af skjulte adfærdsmønstre. I 2018 introducerede en kollega mig for et formelt specifikationssprog kaldet TLA+. Jeg var fanget. Jeg begyndte straks at bygge værktøjer omkring TLA+ og har arbejdet i dette område lige siden.

Du har bygget din karriere omkring formelle metoder og programmeringssprog, fra dit tidlige arbejde med værktøjer baseret på Temporal Logic of Actions (TLA+) til at lede udviklingen af Quint hos Informal Systems. Hvad motiverede dig til at fokusere på at gøre formel verificering mere tilgængelig, og hvordan har den vision formet Quints design?

TLA+ er for godt ikke at blive brugt omfattende i industrien. Jeg var stadig ret junior, da jeg lærte om det, og jeg deltog i møder med mine arbejdskollegaer for at forsøge at finde løsninger sammen, og jeg fandt konstant scenarier, hvor vores løsninger ville fejle. Men jeg var altid den sidste forsvarslinje mod disse scenarier i de fleste tilfælde. Jeg regnede med, at der måtte være en bedre, mindre kostbar og mere værdifuld måde at løse disse scenarier på. Så jeg startede min akademiske rejse mod det, der førte mig til Informal Systems og Quint.

Quint var ikke oprindeligt tænkt som et produkt. Vi byggede det af nødvendighed hos Informal Systems. Vi skrev TLA+-specifikationer for systemer, vi havde brug for at stole mere på, end vi gjorde, men det udvidede sig ikke ud over en meget lille gruppe mennesker, da syntaksen var for skræmmende med for mange matematiske symboler, og værktøjerne mødte ikke folks grundlæggende forventninger. Vi viste kollegaer og eksterne samarbejdspartnere: “se på denne fantastiske ting, jeg har gjort”, men de kunne ikke læse det, og havde ikke tid til at lære et nyt værktøj.

Designvalgene i Quint følger direkte fra den oplevelse. Sproget er let at læse og huske. Den første ting, vi byggede, var en VSCode-udvidelse, der markerer fejl, mens du skriver. Det har typer og forskellige tilstande til at adskille lag eksplicit. Det har en REPL, så du kan udforske interaktivt, og en simulator, så du kan få hurtig feedback og iterere. Det eksporterer spor til en standardiseret JSON-format, der er let for maskiner at parse. Disse var ting, programmører allerede forventede fra deres værktøjer og som vi selv havde brug for. Verificeringen under er den samme logik som TLA+.

Jeg er besat af at gøre formelle metoder mere tilgængelige, og at udgive værktøjer er spændende, men den virkelige effekt føltes kun, hvis ingeniørteam faktisk bruger dem. Der er stadig en delta mellem, hvad værktøjerne kan gøre, og hvor nyttige de føles for udviklere, og jeg arbejder på at lukke den gab.

For læsere, der ikke er fortrolige med det, hvordan ville du forklare, hvad Quint er, og hvorfor et nyt specifikationssprog var nødvendigt sammen med eksisterende værktøjer som TLA+?

De fleste specifikationer er dokumentation. Du skriver ned, hvad systemet skal gøre, og du checker dem ved at læse dem. Problemet er, at dokumentation er forkert på måder, du ikke mekanisk kan registrere: ikke-definerede navne, tvetydig adfærd, underforstået antagelser. Du opdager det normalt under implementering eller i produktion.

En Quint-specifikation er noget, du kan eksekvere. Du modellerer systemet som en tilstandsmaskine, definerer de egenskaber, det skal opfylde, og kører eller verificerer modellen. Hvis der er en overtrædelse, får du et mod eksempel, der viser nøjagtig den sekvens af trin, der udløser det. Det ændrer, hvornår og hvor billigt du fanger en designfejl.

TLA+ kunne altid gøre dette. Quint gør det praktisk for ingeniører, der ikke allerede er specialister i temporal logik.

Quint er designet til at brohøve gab mellem formelle metoder og hverdagssoftware-udvikling. Hvad var de største brugervenlighedsbarrierer, du forsøgte at eliminere i forhold til traditionelle tilgange?

Ærligt talt, var den største brugervenlighedsbarriere syntaksen. Det er derfor, vi startede med syntaksen. Efter at have adresseret det, kunne vi fokusere mere på andre faktorer. Quints type- og effektsystem kom til at markere så mange fejl som muligt, før selv den normale verificeringsproces startede, og folk satte stor pris på det. Det ledte os til at skrive mere højkvalitets-specifikationer, som endnu flere mennesker kunne læse. Vi integrerede det hele i editorer og tilbød den grundlæggende funktionalitet, alle udviklere har ret til at forvente.

Den største effekt efter det var vores simulator. Det startede som en måde at give mennesker den første feedback på systemets adfærd, som en udvikler ønsker at kunne køre koden efter at have skrevet den. Det viste sig at være ekstremt værdifuldt som en måde at få tillid til specifikationer, der er for store til, at verificering kan håndtere, da ekspertisen i at tilpasse en specifikation til at gøre den gennemførlig for verificering ikke skal tages for givet. Vores simulator gjorde tillid mere tilgængelig, og vi har brugt det omfattende i mange projekter.

Mit største smerte punkt med TLA+-syntaksen var, hvor hyppigt jeg blandede mine baglæns- og normale skråstreg. Jeg kan lide Quints syntaks meget bedre, men det, der virkelig gør, at jeg ikke kan gå tilbage, er alle værktøjerne.

En af Quints styrker er dens evne til at modelere og teste distribuerede systemer før implementering. Hvordan ændrer det, hvordan ingeniører skal tænke om at bygge systemer som blockchains eller realtids-infrastruktur?

Den største ændring er at flytte validering tidligere. Leslie Lamport, skaberen af TLA+, sammenligner skrivning af specifikationer før kode med at tegne blåtryk før byggearbejde. Selv hvis du allerede har bygget noget uden et blåtryk, er det stadig en god idé at skrive et nu og bruge det til at informere dine yderligere ændringer.

I software-industrien bruger vi markdown-filer og whiteboards. Måske kan du sammenligne det med at forsøge at tekstligt beskrive en bygning. Det fungerer, men ville du vide, om væggenes størrelse tilføjer op? Quint tilbyder en måde at beskrive systemer, hvor du kan være så højt niveau, som du ønsker, og få indsigt i dets adfærd og korrekthed.

Quint bygger på grundlaget af TLA+, der er bredt anvendt til at beskrive distribuerede systemer. Hvordan balancerede du med at opretholde den teoretiske rigor, mens du gjorde sproget mere udvikler-venligt?

Den nøglebeslutning var at begrænse Quint til en fragment af TLA (logikken bag TLA+) snarere end at eksponere alt, hvad logikken tillader. TLA er meget udtryksfuldt, og noget af den udtryksfuldhed inkluderer operatorer, der ikke er understøttet af nogen værktøjer, og tillader kombinationer, som mennesker forstår og bruger forkert, hvilket gør det rigtigt svært at fejlfinde. Vi traf en bevidst beslutning: fastholde, hvad de fleste realistiske specifikationer faktisk har brug for, og undgå, hvad der har potentiale for forvirring.

Type-systemet og effekt-systemet tilføjer begrænsninger, men begrænsninger, der er nyttige. De forhindrer en hel klasse af spec-fejl, der ikke er sjove, når de opdages efter, at verificeringen allerede er i gang. Typer er næsten fuldstændigt afledt, og effekter er skjult for brugerne, så dette tilføjer værdi uden gnidning.

Før jeg lærte om TLA+’s eksistens, lavede jeg forskningsarbejde i type-systemer, hvilket betyder, at Quints type-afprøver var mit favorit-komponent at skrive. Jeg husker, at jeg drak en Paçoca-smagende kaffe i mine første måneder hos Informal, mens jeg gennemgik et type-system-papir og tænkte “mit liv er fantastisk”.

At gøre sproget godt at bruge, mens man stadig opretholder korrespondance med TLA+ (da Quint-specifikationer kan konverteres til TLA+), var en programmeringssprogs-øvelse, og diskussioner med teamet var den mest nyttige ressource, efterfulgt af feedback fra tidlige brugere. Der er stadig forbedringer, vi ønsker at gøre, og det kan være min yndlingsdel af jobbet.

Du har også arbejdet med statisk analyse og type-systemer. Hvordan har disse oplevelser påvirket Quints type-afprøvning, værktøjer og samlede udvikler-oplevelse?

Den største lære, jeg lærte i den verden, er, at ikke alle sprog er ens. Du hører mennesker sige, at det blot er et spørgsmål om at lære en ny syntaks, alle samme koncepter gælder stadig, så alle sprog er lige og det er blot et spørgsmål om smag. Det er ikke sandt. Feltet programmeringssprog har store forskere, der gør fantastisk arbejde for at fremme dette felt, og det er ikke kun for at gøre et sprog mere smukt eller til deres ønsker.

Funktionel programmering blev introduceret for mig meget tidligt, jeg lærte Haskell på samme tid, som jeg lærte C (mit første programmeringssprog), og jeg er meget taknemlig for det. Dette er grundlaget, der hjælper mig med at se, at isolering af tilstandsændringer og ikke-determinisme til et tyndt lag i Quint og have alle kompleksiteter i rene funktioner objektivt hjælper på mange faktorer, og det er ikke kun et spørgsmål om smag. Jeg tror ikke, at opbygning af Quint ville have været produktiv, hvis spørgsmål om smag var op til diskussion for ofte.

At undervise i formelle metoder som lektor giver dig en unik perspektiv. Hvad er de mest almindelige misforståelser, ingeniører har om formel verificering i dag?

Nå, jeg underviste bachelorstuderende, der lige var begyndt i industrien. Det overvældende flertal af dem havde aldrig hørt om formelle metoder eller formel verificering før, så ingen misforståelser! Kurset var lavet på en måde, så de fleste af dem ikke lærte om distribuerede systemer, og om halvdelen af dem ville lære om tråde i samme semester. Jeg sagde til dem, at jeg følte, jeg underviste dem i, hvad en paraply er godt for, før de havde oplevet nogen regn!

Jeg var mere motiveret til at undervise dem i, hvordan formelle metoder og formel specifikation af et system kan hjælpe os med at resonere om løsninger og finde kanttilfælde end til at få dem til at tro, de skulle formelt verificere alle software, de nogensinde skrev. Min endelige opgave var en bordrollespilsopsætning, hvor forskellige ordrer, spillere kunne tage, og forskellige opsætninger skulle tages i betragtning, og forsøgte at efterligne sværhederne, vi står overfor i distribuerede systemer så meget som muligt. Det lykkedes at være svært nok, så de var nødt til at bruge værktøjerne til at finde kanttilfælde og forbedre deres løsninger til at besejre monstrene til sidst. Jeg håber, at når de står overfor en lignende situation på arbejdet en dag, vil de huske mig. Nogle af dem har allerede gjort det.

Der er en voksende interesse for at kombinere AI med software-udvikling. Ser du en rolle for AI i at hjælpe udviklere med at skrive, validere eller endda generere formelle specifikationer med værktøjer som Quint?

En betydelig en, og det sker allerede. Datalogi er større end at skrive kode, og AI åbner døren til helt nye måder at bruge formelle metoder på. LLM’er er gode til at skrive Quint-specifikationer fra naturlige sprogbeskrivelser af et system og endda eksisterende kode. Quint LLM Kit har Claude Code-agenter, der tager en engelsk beskrivelse af et protokol og producerer en Quint-specifikation, du kan køre og tjekke med det samme.

På samme tid hjælper Quint også udviklere med at stole på kode skrevet med AI. Jeg tror stærkt på, at tillid skal komme fra forståelse, ikke nogle magiske afkrydsningsfelter. Arbejde på en Quint-specifikation, der driver og checker implementeringskoden, betyder, at udviklere stadig kan eje og forstå systemets adfærd, og løse den kognitive gæld, som AI-brug kan skabe, og give mere pålidelige måder at validere den genererede kode på.

Vi udnytter LLM’er som sprog-værktøjer, der skriver Quint-præcise definitioner fra den naturlige sprog-intention, og så giver vi Quint-værktøjerne til AI, så den kan opnå ting, den ikke kan gøre pålideligt på egen hånd, som at finde kanttilfælde.

Set fremad, hvad skal ske for, at formelle metoder kan flytte fra niche-accept til en standarddel af software-udviklingslivscyklussen?

For en stund nu, ved jeg, at de to overordnede ting, Quint har brug for, er lavere omkostninger og højere værdi. Jeg tror, det gælder for mange andre ting også. Formelle metoder fik lige en stor boost i både omkostninger og værdi, med AI, der reducerer omkostningerne ved at skrive formelle specifikationer og også skaber en kontekst af mangel på tillid og forståelse, hvor formelle metoder kan have den største indvirkning og værdi.

Med AI, der ændrer, hvad vores fag er, i hvert fald til en vis grad, håber jeg, at denne ændring er i retning af højere niveau-designvalg og adfærdskorrekthed, og gør formelle metoder til en hverdagsværktøj; og ikke i retning af, at vi ikke forstår nogen kode eller systemer længere og bruger alt vores tid på at gennemgå AI-genereret kode uden nogen værktøjsæt til at hjælpe os med at resonere om det.

Tak for den indsigtsgivende interview; læsere, der er interesseret i at lære mere om dette eksekverbare specifikationssprog til modellering og verificering af komplekse systemer, inklusive dets værktøjer og hvordan man kommer i gang, kan udforske Quint.