Gabriela Moreira, CEO von Quint bei Informal Systems – Interview-Serie

Gabriela Moreira, CEO von Quint bei Informal Systems, ist eine Forschungsingenieurin, die sich auf Programmiersprachen und formale Methoden spezialisiert hat, mit einem starken Fokus auf die Entwicklung von Tools, die die Verifizierung komplexer Systeme für Ingenieure zugänglicher machen. Sie leitet die Entwicklung von Quint, einer modernen ausführbaren Spezifikationssprache, die auf TLA+ basiert, und pflegt und entwickelt die Sprache und ihre Tooling weiter. Ihre Arbeit umfasst formale Verifizierung, statische Analyse und Developer-Tooling, und sie hat auch zur Akademie beigetragen, indem sie formale Methoden unterrichtet, was eine Mischung aus praktischer Ingenieurskunst und theoretischer Tiefe widerspiegelt.

Quint, entwickelt und gewartet bei Informal Systems, ist eine moderne Spezifikationssprache, die zum Modellieren, Testen und Verifizieren komplexer Systeme wie verteilter Netzwerke, Blockchains und Datenbanken konzipiert ist. Basierend auf den Grundlagen der Temporalen Logik von Aktionen (TLA) führt Quint eine entwicklerfreundlichere Syntax ein, zusammen mit erweitertem Tooling wie Typüberprüfung, Simulation und Modellüberprüfung, die es Ingenieuren ermöglichen, Systemfehler vor der Bereitstellung zu erkennen. Die Plattform betont ausführbare Spezifikationen, die es Entwicklern ermöglichen, nicht nur das Systemverhalten zu beschreiben, sondern es auch aktiv zu testen und zu erkunden, und schließt die Lücke zwischen theoretischer Korrektheit und realer Implementierung.

Zurück zum Anfang, was hat Ihr Interesse an der Programmierung initially geweckt, und wie sind Sie schließlich auf formale Methoden und verteilte Systeme gekommen?

Ich war ein eifriger Spieler mit einem schlechten Computer und habe festgestellt, dass ich es genieße, Probleme zu beheben und ihn zum Laufen zu bringen. Ich habe mich für Informatik eingeschrieben und wurde von Theorie und Compilern angezogen. 

Im Jahr 2015 wurde ich mit Programmierwettbewerben konfrontiert. Bei diesen Wettbewerben erhalten Sie normalerweise einige Beispiele für Eingaben und erwartete Ausgaben, und Sie schreiben Code, der das Problem löst und für diese Beispiele funktioniert. Nachdem Sie den Code jedoch zur Bewertung eingereicht haben, wird er tatsächlich mit vielen mehr Beispielen getestet, als Ihnen gezeigt werden. Diese Erkenntnis, dass der Code für die Szenarien, die ich sehe oder von denen ich denke, funktionieren kann, aber dennoch in Fällen, die ich nicht berücksichtigt habe, fehlschlagen kann, hat die Programmierung zu einer Art Herausforderung gemacht, in die ich mich verliebt habe.

In der Industrie wurde ich schnell von verteilten Systemen angezogen, bei denen wir verschiedene Reihenfolgen von Nachrichten berücksichtigen mussten, verschiedene Ausfallmodi und eine ganze Welt von versteckten Verhaltensweisen. Im Jahr 2018 stellte mir ein Kollege eine formale Spezifikationssprache namens TLA+ vor. Ich war sofort begeistert. Ich begann sofort, Tools um TLA+ herum zu bauen und habe seitdem in diesem Bereich gearbeitet.

Sie haben Ihre Karriere um formale Methoden und Programmiersprachen herum aufgebaut, von Ihrer frühen Arbeit an Tooling auf Basis von Temporal Logic of Actions (TLA+) bis hin zur Leitung der Entwicklung von Quint bei Informal Systems. Was hat Sie motiviert, formale Verifizierung zugänglicher zu machen, und wie hat diese Vision die Gestaltung von Quint geprägt?

TLA+ ist zu gut, um nicht umfassend in der Industrie eingesetzt zu werden. Als ich noch relativ neu in der Branche war, lernte ich über TLA+ und nahm an Anrufen mit meinen Kollegen teil, um gemeinsam Lösungen zu finden, und ich stellte fest, dass ich ständig Szenarien fand, in denen unsere Lösungen fehlschlagen würden. Ich war jedoch meist die letzte Verteidigungslinie gegen diese Szenarien in den meisten Fällen. Ich kam zu dem Schluss, dass es einen besseren, weniger kostspieligen und wertvolleren Weg geben muss, diese Szenarien zu lösen. So entstand die Idee, formale Methoden zu verwenden, um Spezifikationen vor der Implementierung von Code zu erstellen. Also begann ich meine akademische Reise in diese Richtung, die mich zu Informal Systems und Quint führte.

Quint war ursprünglich nicht als Produkt konzipiert. Wir bauten es aus Notwendigkeit bei Informal Systems. Wir schrieben TLA+-Spezifikationen für Systeme, denen wir mehr vertrauen mussten, als wir es taten, aber das dehnte sich nicht über eine sehr kleine Gruppe von Menschen aus, da die Syntax zu kompliziert war und das Tooling nicht den grundlegenden Erwartungen der Menschen entsprach. Wir zeigten Kollegen und externen Mitarbeitern: “Sehen Sie sich diese großartige Sache an, die ich gemacht habe”, aber sie konnten es nicht lesen und hatten keine Zeit, ein neues Tool zu lernen.

Die Designentscheidungen in Quint folgen direkt aus dieser Erfahrung. Die Sprache ist leicht zu lesen und zu merken. Das Erste, was wir bauten, war eine VSCode-Erweiterung, die Fehler hervorhebt, während Sie tippen. Sie hat Typen und unterschiedliche Modi, um Schichten explizit zu trennen. Sie hat eine REPL, mit der Sie interaktiv erkunden können, und einen Simulator, mit dem Sie schnelles Feedback erhalten und iterieren können. Sie exportiert Spuren in einem standardisierten JSON-Format, das für Maschinen leicht zu parsen ist. Diese waren Dinge, die Programmierer bereits von ihren Tools erwarten und die wir selbst benötigten. Die Verifizierung darunter ist dieselbe Logik wie TLA+.

Ich bin besessen von der Idee, formale Methoden zugänglicher zu machen, und das Veröffentlichen von Tools ist aufregend, aber der wahre Einfluss wird nur dann wahrgenommen, wenn Ingenieursteams diese tatsächlich verwenden. Es gibt immer noch eine Lücke zwischen dem, was die Tools leisten können, und wie nützlich sie für Entwickler erscheinen, und ich arbeite daran, diese Lücke zu schließen.

Für Leser, die nicht vertraut sind, erklären Sie, was Quint ist und warum eine neue Spezifikationssprache neben bestehenden Tools wie TLA+ benötigt wird.

Die meisten Spezifikationen sind Dokumentation. Sie schreiben auf, was das System tun soll, und überprüfen sie durch Lesen. Das Problem ist, dass Dokumentation auf Weise falsch sein kann, die mechanisch nicht zu erkennen sind: undefinierte Namen, mehrdeutiges Verhalten, implizite Annahmen. Sie stellen normalerweise fest, dass es während der Implementierung oder in der Produktion falsch ist.

Eine Quint-Spezifikation ist etwas, das Sie ausführen. Sie modellieren das System als einen Zustandsautomaten, definieren die Eigenschaften, die es erfüllen soll, und führen oder verifizieren das Modell aus. Wenn es eine Verletzung gibt, erhalten Sie ein Gegenbeispiel, das genau die Sequenz von Schritten zeigt, die es auslöst. Das ändert, wann und wie billig Sie einen Designfehler finden.

TLA+ konnte das immer schon. Quint macht es praktisch für Ingenieure, die keine Spezialisten in temporaler Logik sind.

Quint soll die Lücke zwischen formalen Methoden und alltäglicher Softwareentwicklung schließen. Welche größten Benutzbarkeitsbarrieren haben Sie im Vergleich zu traditionellen Ansätzen beseitigen wollen?

Ehrlich gesagt war die größte Benutzbarkeitsbarriere die Syntax. Deshalb begannen wir mit der Syntax. Nachdem wir diese behoben hatten, konnten wir uns auf andere Faktoren konzentrieren. Quints Typ- und Effektsystem kamen, um so viele Fehler wie möglich vor dem regulären Verifizierungsprozess zu markieren, und die Leute schätzten das sehr. Es führte dazu, dass wir bessere Spezifikationen schrieben, die sogar mehr Menschen lesen konnten. Wir integrierten es in Editoren und boten die grundlegende Funktionalität, die alle Entwickler erwarten dürfen.

Der größte Einfluss danach war unser Simulator. Er begann als einfache Möglichkeit, den Entwicklern erste Rückmeldungen zum Verhalten ihres Systems zu geben, wie ein Entwickler es nach dem Schreiben des Codes möchte. Es stellte sich dann als extrem wertvoll heraus, um Vertrauen in Spezifikationen zu gewinnen, die zu groß für die Verifizierung sind, da die Expertise, eine Spezifikation anzupassen, um sie für die Verifizierung machbar zu machen, nicht vorausgesetzt werden sollte. Unser Simulator machte Vertrauen zugänglicher, und wir haben es in vielen Projekten umfassend eingesetzt.

Mein größter Schmerzpunkt mit der TLA+-Syntax war, wie oft ich meine Rückstriche und regulären Schrägstriche verwechselte, und Sie müssen diese oft tippen. Ich mag Quints Syntax viel besser, aber was mich wirklich daran bindet, ist das gesamte Tooling.

Eine der Stärken von Quint ist die Fähigkeit, verteilte Systeme vor der Bereitstellung zu modellieren und zu testen. Wie ändert sich dadurch die Art und Weise, wie Ingenieure über den Bau von Systemen wie Blockchains oder Echtzeit-Infrastrukturen nachdenken sollten?

Der größte Wandel ist die Verlegung der Validierung nach vorne. Leslie Lamport, der Erfinder von TLA+, vergleicht das Schreiben von Spezifikationen vor dem Code mit dem Zeichnen von Blaupausen vor dem Bau. Selbst wenn Sie bereits etwas ohne Blaupause gebaut haben, ist es immer noch eine gute Idee, eine zu schreiben und sie für weitere Änderungen zu verwenden.

In der Softwareindustrie verwenden wir Markdown-Dateien und Whiteboards. Vielleicht können Sie es mit dem Versuch vergleichen, ein Gebäude textlich zu beschreiben. Es funktioniert, aber wüssten Sie, ob die Größe der Wände zusammenpasst? Quint bietet eine Möglichkeit, Systeme zu beschreiben, bei der Sie so hochwertig sein können, wie Sie möchten, und Erkenntnisse über ihr Verhalten und ihre Korrektheit erhalten.

Quint basiert auf den Grundlagen von TLA+, die weit verbreitet zur Beschreibung von verteilten Systemen verwendet werden. Wie haben Sie es geschafft, die theoretische Strenge beizubehalten, während Sie die Sprache benutzerfreundlicher gemacht haben?

Die wichtigste Entscheidung war, Quint auf einen Teil von TLA (der Logik hinter TLA+) zu beschränken, anstatt alles, was die Logik ermöglicht, offenzulegen. TLA ist sehr ausdrucksstark, und einige dieser Ausdrucksstärke umfassen Operatoren, die von keinen Tools unterstützt werden und Kombinationen, die die Leute falsch verstehen und verwenden, was es sehr schwierig macht, Fehler zu finden. Wir haben eine bewusste Entscheidung getroffen: Wir bleiben bei dem, was die meisten realistischen Spezifikationen tatsächlich benötigen, und vermeiden das, was das Potenzial für Verwirrung hat.

Das Typsystem und das Effektsystem fügen Einschränkungen hinzu, aber nützliche Einschränkungen. Sie verhindern eine ganze Klasse von Spezifikationsfehlern, die nicht lustig sind, wenn sie nach dem Start des Verifizierungsprozesses gefunden werden. Typen werden fast vollständig abgeleitet und Effekte sind für die Benutzer verborgen, sodass dies einen Wert ohne Reibung hinzufügt.

Bevor ich von der Existenz von TLA+ erfuhr, arbeitete ich an Forschungsarbeiten zu Typsystemen, was bedeutet, dass der Typprüfer von Quint wahrscheinlich mein Lieblingskomponent war, den ich zu schreiben hatte. Ich erinnere mich, dass ich in meinen ersten Monaten bei Informal Systems einen Paçoca-geschmackenen Kaffee trank, während ich einen Typsystem-Artikel überprüfte und dachte: “Mein Leben ist großartig”. 

Die Sprache gut zu machen, während sie immer noch mit TLA+ korrespondiert (da Quint-Spezifikationen in TLA+ transpiliert werden können), war eine Programmiersprachenaufgabe, und Diskussionen mit dem Team waren die hilfreichste Ressource, gefolgt von Feedback von frühen Benutzern. Es gibt immer noch Verbesserungen, die wir vornehmen möchten, und es könnte mein Lieblingsteil der Arbeit sein.

Sie haben auch an statischer Analyse und Typsystemen gearbeitet. Wie haben diese Erfahrungen die Typüberprüfung, das Tooling und die gesamte Entwicklererfahrung von Quint beeinflusst?

Die größte Lektion, die ich in dieser Welt gelernt habe, ist, dass nicht alle Sprachen gleich sind. Sie werden Menschen hören, die sagen, es sei nur eine Frage des Lernens einer neuen Syntax, alle Konzepte seien gleich, also seien alle Sprachen gleich und es sei nur eine Frage des Geschmacks. Das ist nicht wahr. Das Feld der Programmiersprachen hat großartige Forscher, die hervorragende Arbeit leisten, um dieses Feld voranzutreiben, und das ist nicht nur, um eine Sprache hübscher oder mehr nach ihrem Geschmack zu machen.

Funktionale Programmierung wurde mir sehr früh vorgestellt, ich lernte Haskell zur gleichen Zeit wie C (meine erste Programmiersprache), und ich bin sehr dankbar dafür. Dies ist die Grundlage, die mir hilft, zu sehen, dass die Isolierung von Zustandsmutationen und Nichtdeterminismus in einer dünnen Schicht in Quint und das Haben aller Komplexität in reinen Funktionen objektiv hilft, und es ist nicht nur eine Frage des Geschmacks. Ich denke nicht, dass das Bauen von Quint produktiv gewesen wäre, wenn Fragen des Geschmacks oft zur Diskussion gestellt worden wären.

Das Unterrichten von formalen Methoden als Dozent gibt Ihnen eine einzigartige Perspektive. Welche sind die häufigsten Missverständnisse, die Ingenieure über formale Verifizierung heute haben?

Nun, ich unterrichtete Studenten im Grundstudium, die gerade erst in die Branche eintraten. Die überwiegende Mehrheit von ihnen hatte noch nie von formalen Methoden oder formalen Verifizierungen gehört, also gab es keine Missverständnisse! Der Lehrplan war so gestaltet, dass die meisten von ihnen auch nicht über verteilte Systeme oder Threads in demselben Semester lernten. Ich sagte ihnen, ich fühle mich, als ob ich ihnen erkläre, was ein Regenschirm gut für ist, bevor sie je Regen erlebt haben!

Ich war mehr motiviert, ihnen beizubringen, wie formale Methoden und das formale Spezifizieren eines Systems helfen können, Lösungen zu finden und Randfälle zu finden, als sie dazu zu bringen, zu denken, sie sollten jeden Software-Code, den sie je schreiben, formal verifizieren. Meine Abschlussarbeit war ein Tabletop-RPG-Setup, bei dem unterschiedliche Reihenfolgen, die Spieler nehmen konnten, und unterschiedliche Aufstellungen berücksichtigt werden mussten, um die Schwierigkeiten, die wir in verteilten Systemen haben, so gut wie möglich nachzubilden. Es war erfolgreich, weil es schwierig genug war, dass sie die Tools verwenden mussten, um Randfälle zu finden und ihre Lösungen zu verbessern, um die Monster am Ende zu besiegen. Hoffentlich werden sie, wenn sie sich in einer ähnlichen Situation bei der Arbeit wiederfinden, an mich denken. Einige von ihnen haben es bereits getan.

Gibt es eine Rolle für künstliche Intelligenz bei der Unterstützung von Entwicklern beim Schreiben, Validieren oder sogar Generieren formaler Spezifikationen mit Tools wie Quint?

Eine bedeutende Rolle, und sie ist bereits im Gange. Informatik ist größer als das Schreiben von Code, und künstliche Intelligenz öffnet die Tür zu völlig neuen Möglichkeiten, formale Methoden zu verwenden. LLMs sind gut darin, Quint-Spezifikationen aus natürlichen Sprachbeschreibungen von Systemen und sogar vorhandenem Code zu schreiben. Der Quint-LLM-Kit hat Claude-Code-Agents, die eine englische Beschreibung eines Protokolls nehmen und eine Quint-Spezifikation erzeugen, die Sie sofort ausführen und überprüfen können.

Gleichzeitig hilft Quint auch dabei, Code, der mit künstlicher Intelligenz geschrieben wird, zu vertrauen. Ich glaube fest, dass Vertrauen aus Verständnis kommen muss, nicht aus magischen Häkchen. Die Arbeit an einer Quint-Spezifikation, die die Implementierung des Codes antreibt und überprüft, bedeutet, dass Entwickler immer noch das Verhalten des Systems besitzen und verstehen können, was die kognitive Schulden, die die Verwendung von künstlicher Intelligenz erzeugen kann, angeht und assertive Wege zur Validierung des generierten Codes bietet.

Wir nutzen LLMs als Sprachtools, die Quint-Präzisionsdefinitionen aus natürlicher Sprachabsicht schreiben, und geben dann die Quint-Tools an die künstliche Intelligenz, damit sie Dinge tun kann, die sie alleine nicht zuverlässig tun kann, wie das Finden von Randfällen.

Blickt man in die Zukunft, was muss geschehen, damit formale Methoden von einer Nischenadoption zu einem Standardteil des Softwareentwicklungslebenszyklus werden?

Für eine Weile jetzt weiß ich, dass die beiden wichtigsten Dinge, die Quint für mehr Akzeptanz benötigt, sind: geringere Kosten und höherer Wert. Ich denke, das gilt auch für viele andere Dinge. Formale Methoden haben gerade einen großen Schub in beiden Dingen erhalten, da künstliche Intelligenz die Kosten für das Schreiben formaler Spezifikationen enorm reduziert hat und auch eine Umgebung der mangelnden Vertrauens und des mangelnden Verständnisses geschaffen hat, in der formale Methoden am meisten Einfluss und Wert haben können.

Mit der künstlichen Intelligenz, die unser Berufsbild verändert, zumindest in einem gewissen Maße, hoffe ich, dass diese Veränderung in Richtung höherer Designentscheidungen und Verhaltenskorrektheit führt, was formale Methoden zu einem alltäglichen Werkzeug macht; und nicht dazu, dass wir kein Code oder System mehr verstehen und unsere ganze Zeit damit verbringen, künstlich generierten Code ohne jedes Toolset zu überprüfen, das uns hilft, darüber nachzudenken.

Vielen Dank für das aufschlussreiche Interview; Leser, die mehr über diese ausführbare Spezifikationssprache für das Modellieren und Verifizieren komplexer Systeme erfahren möchten, einschließlich ihrer Tooling und wie man loslegt, können Quint erkunden.