Gabriela Moreira, administrerende direktør for Quint i Informal Systems – Interviewserie

Gabriela Moreira, administrerende direktør for Quint i Informal Systems, er en forskningsingeniør, der specialiserer sig i programmeringssprog og formelle metoder, med stærkt fokus på at udvikle værktøjer, der gør kompleks systemverifikation mere tilgængelig for ingeniører. Hun står i spidsen for udviklingen af Quint, et moderne specifikationssprog baseret på TLA+, hvor hun fortsat vedligeholder og udvikler sproget og dets værktøjer. Hendes arbejde omfatter formel verifikation, statisk analyse og udvikler-væ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 i Informal Systems, er et moderne specifikationssprog designet til at modelere, teste og verificere komplekse systemer som f.eks. distribuerede netværk, blockchains og databases. Bygget på grundlag af Temporal Logic of Actions (TLA), introducerer Quint en mere udvikler-venlig syntaks samt avanceret værktøj som type-tjek, simulation og model-tjek, 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.

Hvad var det, der først vækkede din interesse for programmering, og hvordan kom du til at arbejde med formelle metoder og distribuerede systemer?

Jeg var en ivrig gamer med en dårlig computer, og jeg indså, at jeg nød at løse problemerne og få det til at virke. Jeg tilmeldte mig computervidenskab og blev draget til teori og kompilatorer. 

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

Da jeg arbejdede i industrien, blev jeg hurtigt draget til distribuerede systemer, hvor vi skulle overveje forskellige ordninger af beskeder, der kunne ankomme, forskellige fejltilstande og en hel verden af skjulte beteende. I 2018 introducerede en kollega mig til et formelt specifikationssprog kaldet TLA+. Jeg var fanget. Jeg startede straks med 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 i Informal Systems. Hvad motiverede dig til at fokusere på at gøre formel verifikation mere tilgængelig, og hvordan har denne vision formet Quints design?

TLA+ er for godt ikke at blive brugt omfattende i industrien. Da jeg stadig var ret ung, lærte jeg om det, og jeg ville deltage i møder med mine kollegaer for at prøve 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 indså, 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, som førte mig til Informal Systems og Quint.

Quint var ikke oprindeligt koncepteret som et produkt. Vi byggede det af nødvendighed i Informal Systems. Vi skrev TLA+-specifikationer for systemer, vi havde brug for at stole på mere, 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 denne erfaring. Sproget er let at læse og huske. Det første, vi byggede, var en VSCode-udvidelse, der fremhæver fejl, mens du skriver. Det har typer og distinkte 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. Verifikationen 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øles kun, hvis ingeniørhold 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 denne gap.

For læsere, der ikke er bekendt 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 opdage: ikke-definerede navne, tvetydig adfærd, implicit 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øre eller verificere modellen. Hvis der er en overtrædelse, får du et mod eksempel, der viser præcis 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 brokke gapet 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 effekt-system kom til at flagge så mange fejl som muligt, før man overhovedet startede den normale verifikationsproces, 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. Den startede som en måde at tilbyde folk den første feedback på systemets adfærd, som en udvikler ønsker at kunne, på en eller anden måde, 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 verifikation kan håndtere, da ekspertisen i at tilpasse en specifikation til at gøre den mulig for verifikation 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 ofte jeg blandede mine bakslashes og almindelige slashes, og du skal skrive dem meget. 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 dette, 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 beskrive en bygning tekstligt. Det virker, men ville du vide, om væggenes størrelse passer sammen? 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 brugt til at beskrive distribuerede systemer. Hvordan balancerede du med at opretholde denne teoretiske rigor, samtidig med at gøre sproget mere udvikler-venligt?

Den afgørende beslutning var at begrænse Quint til en delmængde af TLA (logikken bag TLA+) snarere end at eksponere alt, hvad logikken tillader. TLA er meget udtryksfuldt, og noget af denne udtryksfuldhed inkluderer operatore, der ikke understøttes af nogen værktøjer, og tillader kombinationer, som mennesker forstår og bruger forkert, hvilket gør det virkelig svært at fejlfinde. Vi traf en bevidst beslutning: fasthold, 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 verifikationen allerede kører. 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-checker sandsynligvis var mit favorit-komponent at skrive. Jeg husker at drikke 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, samtidig med at opretholde korrespondance med TLA+ (da Quint-specifikationer kan konverteres til TLA+), var en programmeringssprog-øvelse, og diskussioner med holdet 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 erfaringer påvirket Quints type-check, værktøjer og samlede udvikler-oplevelse?

Den største lære, jeg fik 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 kun en smagssag. Det er ikke sandt. Feltet af 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 mere til deres smag.

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 havde alle kompleksiteter i rene funktioner objektivt hjælper med mange faktorer, og det er ikke kun en smagssag. Jeg tror ikke, at opbygning af Quint ville have været produktiv, hvis smagssager var op til diskussion ofte.

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

Vel, jeg underviste bachelorstuderende, der lige var begyndt i industrien. Det overvældende flertal af dem havde aldrig hørt om formelle metoder eller formel verifikation før, så ingen misforståelser! Kurriculummet var lavet på en måde, så de fleste af dem også ikke lærte om distribuerede systemer, og om halvdelen af dem ville lære om tråde i samme semester. Jeg fortalte 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 forstå løsninger og finde edge-cases, end til at få dem til at tro, at de skulle formelt verificere hver software, de nogensinde skrev. Min sidste opgave var en bordrollespilsopsætning, hvor forskellige ordninger, spillere kunne tage, og forskellige opsætninger skulle tages i betragtning, og prøve 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 måtte bruge værktøjerne til at finde edge-cases 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, validerer eller endda generere formelle specifikationer med værktøjer som Quint?

En betydelig en, og det sker allerede. Computer Science 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 en 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 checkmark. Arbejde på en Quint-specifikation, der driver og checker implementeringskoden, betyder, at udviklere stadig kan eje og forstå systemets adfærd, og adressere den kognitive gæld, som AI-brug kan skabe, og giver 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 edge-cases.

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

For en periode nu ved jeg, at de to højt niveau-ting, Quint har brug for for mere accept, er lavere omkostninger og højere værdi. Jeg tror, dette gælder for mange andre ting også. Formelle metoder fik lige en stor boost i både disse to ting, med AI, der reducerer omkostningerne ved at skrive formelle specifikationer og også skaber en miljø, hvor manglen på tillid og forståelse kan gøre formelle metoder mest påvirkelige og værdifulde.

Med AI, der ændrer, hvad vores profession er, i hvert fald til en vis grad, håber jeg, at denne ændring er i retning af højere niveau-designvalg og adfærds-korrekthed, 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 forstå det.

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