Gabriela Moreira, CEO van Quint bij Informal Systems – Interviewreeks

Gabriela Moreira, CEO van Quint bij Informal Systems, is een onderzoeksingenieur die zich specialiseert in programmeertalen en formele methoden, met een sterke focus op het ontwikkelen van tools die complexe systeemverificatie toegankelijker maken voor ingenieurs. Ze leidt de ontwikkeling van Quint, een moderne uitvoerbare specificatietaal gebaseerd op TLA+, waar ze de taal en de tooling blijft onderhouden en ontwikkelen. Haar werk omvat formele verificatie, statische analyse en ontwikkelaarstooling, en ze heeft ook bijgedragen aan de academische wereld door formele methoden te onderwijzen, wat een combinatie is van praktische ingenieurskunst en theoretische diepgang.

Quint, ontwikkeld en onderhouden bij Informal Systems, is een moderne specificatietaal ontworpen om complexe systemen zoals gedistribueerde netwerken, blockchains en databases te modelleren, testen en verifiëren. Gebouwd op de fundamenten van de Temporal Logic of Actions (TLA), introduceert Quint een meer ontwikkelaarvriendelijke syntaxis, evenals geavanceerde tooling zoals typecontrole, simulatie en modelcontrole, waardoor ingenieurs systeemfouten kunnen detecteren voordat ze worden geïmplementeerd. Het platform legt de nadruk op uitvoerbare specificaties, waardoor ontwikkelaars niet alleen systeemgedrag kunnen beschrijven, maar het ook actief kunnen testen en onderzoeken, waardoor de kloof tussen theoretische correctheid en praktische implementatie wordt overbrugd.

Terug naar het begin, wat heeft uw interesse in programmeren gewekt, en hoe bent u uiteindelijk in formele methoden en gedistribueerde systemen terechtgekomen?

Ik was een fervente gamer met een slechte computer, en ik realiseerde me dat ik genoot van het oplossen van problemen en het maken ervan. Ik schreef me in voor informatica en werd aangetrokken door theorie en compilers.

In 2015 werd ik geconfronteerd met programmeerwedstrijden. Daarin krijg je meestal een paar voorbeelden van invoer en verwachte uitvoer, en je schrijft code die het probleem oplost en werkt voor die voorbeelden. Echter, nadat je het hebt ingediend voor evaluatie, wordt de code daadwerkelijk getest met veel meer voorbeelden dan degenen die ze je laten zien. Die realisatie dat code kan werken voor de scenario’s die ik zie of waar ik aan denk, maar nog steeds falen in gevallen die ik niet heb overwogen, maakte programmeren tot een soort uitdaging waar ik verliefd op werd.

Terwijl ik in de industrie werkte, werd ik snel aangetrokken door gedistribueerde systemen, waar we verschillende bestellingen van berichten moesten overwegen, verschillende foutmodi en een hele wereld van verborgen gedragingen. In 2018 stelde een collega me voor aan een formele specificatietaal genaamd TLA+. Ik was meteen verkocht. Ik begon meteen tools te bouwen rond TLA+ en heb sindsdien in deze ruimte gewerkt.

U hebt uw carrière opgebouwd rond formele methoden en programmeertalen, van uw vroege werk aan tooling op basis van Temporal Logic of Actions (TLA+) tot het leiden van de ontwikkeling van Quint bij Informal Systems. Wat heeft u gemotiveerd om formele verificatie toegankelijker te maken, en hoe heeft die visie de ontwerpkeuzes van Quint beïnvloed?

TLA+ is te goed om niet uitgebreid in de industrie te worden gebruikt. Ik was nog vrij junior toen ik het leerde kennen, en ik voegde me bij deze calls met mijn collega’s om samen oplossingen te proberen te vinden, en ik vond altijd scenario’s waarin onze oplossingen zouden falen. Echter, ik was altijd de laatste verdedigingslinie tegen die scenario’s in de meeste gevallen. Ik dacht dat er een betere, minder dure, meer waardevolle manier moest zijn om die scenario’s op te lossen. Dus ik begon mijn academische reis ernaartoe, wat me naar Informal Systems en Quint leidde.

Quint was oorspronkelijk niet bedoeld als een product. We bouwden het uit noodzaak bij Informal Systems. We schreven TLA+-specificaties voor systemen die we meer vertrouwden dan we deden, maar dat breidde zich niet uit buiten een zeer kleine groep mensen, omdat de syntaxis te eng was met te veel wiskundige symbolen, en de tooling voldeed niet aan de basisverwachtingen van de mensen. We toonden collega’s en externe medewerkers: “kijk naar dit geweldige ding dat ik heb gedaan”, maar ze konden het niet lezen en hadden geen tijd om een nieuwe tool te leren.

De ontwerpkeuzes in Quint volgen rechtstreeks uit die ervaring. De taal is gemakkelijk te lezen en te onthouden. Het eerste dat we bouwden was een VSCode-extensie die fouten markeert terwijl je typt. Het heeft typen en verschillende modi om lagen expliciet te scheiden. Het heeft een REPL zodat je interactief kunt onderzoeken, en een simulator zodat je snel feedback kunt krijgen en itereren. Het exporteert sporen naar een gestandaardiseerd JSON-formaat dat gemakkelijk door machines kan worden geparseerd. Dit waren dingen die programmeurs al verwachtten van hun tools en die wij zelf nodig hadden. De verificatie eronder is dezelfde logica als TLA+.

Ik ben geobsedeerd door het maken van formele methoden toegankelijker, en het verzenden van tools is spannend, maar de echte impact wordt alleen gevoeld als ingenieursgroepen ze daadwerkelijk gebruiken. Er is nog een delta tussen wat de tools kunnen doen en hoe nuttig ze voor ontwikkelaars aanvoelen, en ik werk aan het dichten van die kloof.

Voor lezers die hier niet mee bekend zijn, hoe zou u uitleggen wat Quint is en waarom een nieuwe specificatietaal nodig was naast bestaande tools zoals TLA+?

De meeste specificaties zijn documentatie. U schrijft op wat het systeem moet doen, en u controleert ze door ze te lezen. Het probleem is dat documentatie op manieren verkeerd kan zijn die mechanisch niet te detecteren zijn: ongedefinieerde namen, dubbelzinnig gedrag, impliciete veronderstellingen. U ontdekt ze meestal tijdens de implementatie of in productie.

Een Quint-specificatie is iets dat u uitvoert. U modelleert het systeem als een statemachine, definieert de eigenschappen die het moet vervullen, en voert of verifieert het model uit. Als er een schending is, krijgt u een tegenvoorbeeld dat exact de reeks stappen toont die het triggeren. Dat verandert wanneer en hoe goedkoop u een ontwerpfout kunt vangen.

TLA+ kon dit altijd al. Quint maakt het praktisch voor ingenieurs die nog geen specialisten zijn in temporale logica.

Quint is ontworpen om de kloof tussen formele methoden en alledaagse software-ontwikkeling te overbruggen. Wat waren de grootste bruikbaarheidsbarrières die u wilde elimineren in vergelijking met traditionele benaderingen?

Eerlijk gezegd was de grootste bruikbaarheidsbarrière de syntaxis. Dat is waarom we begonnen met de syntaxis. Nadat we dat hadden aangepakt, konden we ons meer richten op andere factoren. Quint’s type- en effectensysteem kwamen om zo veel mogelijk fouten te markeren voordat de reguliere verificatieproces begon, en mensen waardeerden dat zeer. Het leidde ertoe dat we meer kwalitatief hoogwaardige specificaties schreven die nog meer mensen konden lezen. We integreerden het allemaal in editors en boden de basisfunctionaliteit die alle ontwikkelaars het recht hebben om te verwachten.

De grootste impact daarna was onze simulator. Het begon als een manier om mensen eerst feedback te geven over het gedrag van hun systeem, zoals een ontwikkelaar wil kunnen doen, nadat hij de code heeft geschreven. Het bleek extreem waardevol te zijn als een manier om vertrouwen te krijgen in specificaties die te groot zijn voor verificatie om aan te kunnen. Onze simulator maakte vertrouwen toegankelijker en we hebben het uitgebreid gebruikt in veel projecten.

Mijn grootste pijnpunt met TLA+-syntaxis was hoe vaak ik mijn backslashes en reguliere slashes mengde, en je moet die veel typen. Ik vind Quint’s syntaxis veel beter, maar wat het echt onmogelijk maakt om terug te gaan voor mij is alle tooling.

Een van Quint’s sterktes is zijn vermogen om gedistribueerde systemen te modelleren en te testen voordat ze worden geïmplementeerd. Hoe verandert dit de manier waarop ingenieurs moeten denken over het bouwen van systemen zoals blockchains of real-time-infrastructuur?

De grootste verschuiving is validatie eerder verplaatsen. Leslie Lamport, de maker van TLA+, vergelijkt het schrijven van specificaties voordat code wordt geschreven met het tekenen van blauwdrukken voordat constructiewerk wordt uitgevoerd. Zelfs als je al iets hebt gebouwd zonder blauwdruk, is het nog steeds een goed idee om er een te schrijven en het te gebruiken om je verdere veranderingen te informeren.

In de software-industrie gebruiken we markdown-bestanden en whiteboards. Misschien kunt u het vergelijken met het proberen om een gebouw tekstueel te beschrijven. Het werkt, maar zou u weten of de wandgrootte bij elkaar past? Quint biedt een manier om systemen te beschrijven waar u zo hoog niveau kunt zijn als u wilt, en inzicht krijgt in zijn gedrag en correctheid.

Quint bouwt voort op de fundamenten van TLA+, die breed wordt gebruikt om gedistribueerde systemen te beschrijven. Hoe hebt u de theoretische rigor in stand gehouden terwijl u de taal meer ontwikkelaarvriendelijk maakte?

De sleutelbeslissing was om Quint te beperken tot een fragment van TLA (de logica achter TLA+) in plaats van alles wat de logica toelaat. TLA is zeer expressief, en sommige van die expressiviteit omvat operatoren die niet door enige tool worden ondersteund, en laat combinaties toe die mensen verkeerd begrijpen en gebruiken, waardoor het echt moeilijk wordt om te debuggen. We maakten een bewuste keuze: houd vast aan wat de meeste realistische specificaties eigenlijk nodig hebben, en vermijd wat potentieel voor verwarring zorgt.

Het typesysteem en effectensysteem voegen beperkingen toe, maar beperkingen die nuttig zijn. Ze voorkomen een hele klasse specificatiefouten die niet leuk zijn als ze worden gevonden nadat de verificatie al loopt. Types worden bijna geheel afgeleid en effecten worden voor gebruikers verborgen, dus dit voegt waarde toe met geen enkele wrijving.

Voordat ik van het bestaan van TLA+ hoorde, deed ik onderzoekswerk in typesystemen, wat betekent dat Quint’s typechecker waarschijnlijk mijn favoriete component was om te schrijven. Ik herinner me dat ik een Paçoca-geflavoreerde koffie dronk in mijn eerste paar maanden bij Informal terwijl ik een paper over het typesysteem bekeek en dacht: “mijn leven is geweldig”.

Het maken van de taal goed te gebruiken terwijl nog steeds overeenstemming met TLA+ te houden (aangezien Quint-specificaties kunnen worden omgezet in TLA+) was een programmeertaalopgave, en discussies met het team waren de meest behulpzame bron, gevolgd door feedback van vroege gebruikers. Er zijn nog verbeteringen die we willen maken, en het kan mijn favoriete deel van de baan zijn.

U hebt ook gewerkt aan statische analyse en typesystemen. Hoe hebben die ervaringen Quint’s typecontrole, tooling en algemene ontwikkelaarservaring beïnvloed?

De grootste les die ik in die wereld heb geleerd is dat niet alle talen hetzelfde zijn. U zult mensen horen zeggen dat het alleen maar een kwestie is van het leren van een nieuwe syntaxis, allemaal dezelfde concepten gelden nog steeds, dus alle talen zijn gelijk en het is alleen een kwestie van smaak. Dat is niet waar. Het veld van programmeertalen heeft grote onderzoekers die geweldig werk doen om dit veld te bevorderen, en dat is niet alleen om een taal er mooier of meer naar hun zin te maken.

Functionele programmering werd me vroeg ingevoerd, ik leerde Haskell op hetzelfde moment dat ik C leerde (mijn eerste programmeertaal), en ik ben daar erg dankbaar voor. Dit is de basis die me helpt om te zien dat het isoleren van staatmutaties en niet-determinisme tot een dunne laag in Quint, en het hebben van alle complexiteit in pure functies, objectief helpt bij veel factoren, en het is niet alleen een kwestie van smaak. Ik denk niet dat het bouwen van Quint productief zou zijn geweest als kwesties van smaak vaak ter discussie stonden.

Het onderwijzen van formele methoden als docent geeft u een uniek perspectief. Wat zijn de meest voorkomende misvattingen die ingenieurs hebben over formele verificatie vandaag de dag?

Nou, ik gaf les aan undergraduate-studenten die net in de industrie begonnen. De overgrote meerderheid van hen had nog nooit van formele methoden of formele verificatie gehoord, dus geen misvattingen! Het curriculum was zo opgesteld dat de meesten van hen ook niet over gedistribueerde systemen leerden, en ongeveer de helft van hen zou leren over threads in hetzelfde semester. Ik zei tegen hen dat ik me voelde alsof ik ze uitlegde wat een paraplu voor is voordat ze ooit regen hadden meegemaakt!

Ik was meer gemotiveerd om hen te leren hoe formele methoden en formeel specificeren van een systeem ons kunnen helpen om oplossingen te beredeneren en randgevallen te vinden dan om hen te laten denken dat ze elke software die ze ooit schrijven formeel moeten verifiëren. Mijn eindopdracht was een tafelrollenspel-opstelling waarin verschillende bestellingen die spelers konden nemen en verschillende opstellingen moesten worden overwogen, proberend om de moeilijkheden die we in gedistribueerde systemen tegenkomen zo veel mogelijk na te bootsen. Het lukte om moeilijk genoeg te zijn dat ze de tools moesten gebruiken om randgevallen te vinden en hun oplossingen te verbeteren om de monsters uiteindelijk te verslaan. Hopelijk zullen ze, wanneer ze ooit in een soortgelijke situatie terechtkomen op het werk, aan mij denken. Sommigen van hen deden dat al.

Er is een groeiende interesse in het combineren van AI met software-ontwikkeling. Ziet u een rol voor AI in het helpen van ontwikkelaars bij het schrijven, valideren of zelfs genereren van formele specificaties met behulp van tools zoals Quint?

Een significante, en het gebeurt al. Informatica is groter dan code schrijven, en AI opent de deur naar volledig nieuwe manieren van het gebruik van formele methoden. LLM’s zijn goed in het schrijven van Quint-specificaties vanuit natuurlijke taalbeschrijvingen van een systeem en zelfs bestaande code. De Quint LLM Kit heeft Claude Code-agents die een Engelse beschrijving van een protocol nemen en een Quint-specificatie produceren die u kunt uitvoeren en controleren.

Tegelijkertijd helpt Quint ook ontwikkelaars om code te vertrouwen die met AI is geschreven. Ik geloof sterk dat vertrouwen moet komen van begrip, niet van enkele magische vinkjes. Werken aan een Quint-specificatie die de implementatiecode aandrijft en controleert, betekent dat ontwikkelaars nog steeds de gedragingen van het systeem kunnen begrijpen en bezitten, waardoor de cognitieve schuld die AI-gebruik kan creëren wordt aangepakt en er assertievere manieren zijn om gegenereerde code te valideren.

We gebruiken LLM’s als taaltools die Quint-precise definities schrijven vanuit de natuurlijke taalintentie, en geven dan de Quint-tools aan AI zodat het dingen kan doen die het zelf niet betrouwbaar kan doen, zoals het vinden van randgevallen.

Kijkend naar de toekomst, wat moet er gebeuren om formele methoden van niche-adoptie naar een standaardonderdeel van de software-ontwikkelingscyclus te brengen?

Voor een tijdje weet ik dat de twee hoogste dingen die Quint nodig heeft voor meer adoptie: lagere kosten en hogere waarde. Ik denk dat dit van toepassing is op veel andere dingen. Formele methoden kregen net een grote boost in zowel kosten als waarde, met AI die de kosten van het schrijven van formele specificaties aanzienlijk verlaagt en ook een omgeving van gebrek aan vertrouwen en begrip creëert waar formele methoden het meest impactvol en waardevol kunnen zijn.

Met AI die onze professie verandert, tenminste tot op zekere hoogte, hoop ik dat deze verandering is naar hogere ontwerpkeuzes en gedragscorrectheid, waardoor formele methoden een alledaags instrument worden; en niet naar ons niet begrijpen van enige code of systemen en ons hele tijd besteden aan het herzien van AI-gegenereerde code zonder enig instrument om ons te helpen redeneren.

Bedankt voor het inspirerende interview; lezers die meer willen leren over deze uitvoerbare specificatietaal voor het modelleren en verifiëren van complexe systemen, inclusief de tooling en hoe te beginnen, kunnen Quint verkennen.