Gabriela Moreira, PDG de Quint chez Informal Systems – Série d’entretiens

Gabriela Moreira, PDG de Quint chez Informal Systems, est une ingénieure de recherche spécialisée dans les langages de programmation et les méthodes formelles, avec un fort accent sur la création d’outils qui rendent la vérification de systèmes complexes plus accessible aux ingénieurs. Elle dirige le développement de Quint, un langage de spécification exécutable moderne basé sur TLA+, où elle continue de maintenir et de faire évoluer le langage et ses outils. Son travail s’étend à la vérification formelle, à l’analyse statique et à l’outillage de développement, et elle a également contribué à l’enseignement universitaire en enseignant les méthodes formelles, reflétant un mélange d’ingénierie pratique et de profondeur théorique.

Quint, développé et maintenu par Informal Systems, est un langage de spécification moderne conçu pour modéliser, tester et vérifier des systèmes complexes tels que les réseaux distribués, les blockchains et les bases de données. Fondé sur les fondements de la logique temporelle des actions (TLA), Quint introduit une syntaxe plus conviviale pour les développeurs, ainsi que des outils avancés tels que la vérification de types, la simulation et la vérification de modèles, permettant aux ingénieurs de détecter les défaillances du système avant leur déploiement. La plateforme met l’accent sur les spécifications exécutables, permettant aux développeurs de décrire non seulement le comportement du système, mais également de le tester et de l’explorer activement, en comblant le fossé entre la correction théorique et la mise en œuvre dans le monde réel.

En revenant au début, qu’est-ce qui a d’abord suscité votre intérêt pour la programmation, et comment avez-vous finalement trouvé votre chemin dans les méthodes formelles et les systèmes distribués ?

J’étais une joueuse passionnée avec un mauvais ordinateur, et j’ai réalisé que j’aimais résoudre les problèmes et le faire fonctionner. J’ai inscrit à la science informatique et j’ai été attirée par la théorie et les compilateurs.

En 2015, j’ai été présentée à des concours de programmation. Dans ceux-ci, vous obtenez généralement quelques exemples d’entrée et de sortie attendue, et vous écrivez du code qui résout le problème et fonctionne pour ces exemples. Cependant, après avoir soumis le code pour évaluation, il est en fait testé avec beaucoup plus d’exemples au-delà de ceux qu’ils vous montrent. Cette réalisation que le code pourrait fonctionner pour les scénarios que je vois ou que je pense, mais qu’il pourrait encore échouer dans des cas que je n’ai pas considérés, a rendu la programmation un défi que j’ai adoré.

En travaillant dans l’industrie, j’ai été rapidement attirée par les systèmes distribués, où nous devions considérer différents ordres dans lesquels les messages pouvaient arriver, différents modes de défaillance et un monde entier de comportements cachés. En 2018, un collègue m’a présenté un langage de spécification formelle appelé TLA+. J’étais accro. J’ai immédiatement commencé à construire des outils autour de TLA+ et j’ai travaillé dans cet espace depuis.

Vous avez construit votre carrière autour des méthodes formelles et des langages de programmation, de votre travail précoce sur les outils basés sur la logique temporelle des actions (TLA+) à la direction du développement de Quint chez Informal Systems. Qu’est-ce qui vous a motivée à vous concentrer sur le fait de rendre la vérification formelle plus accessible, et comment cette vision a-t-elle façonné la conception de Quint ?

TLA+ est trop bon pour ne pas être utilisé de manière extensive dans l’industrie. J’étais encore assez junior lorsque j’ai appris à son sujet, et je me joignais à ces appels avec mes collègues de travail pour essayer de trouver des solutions ensemble, et je constatais constamment des scénarios dans lesquels nos solutions échoueraient. Cependant, j’étais toujours la dernière ligne de défense contre ces scénarios dans la plupart des cas. J’ai décidé qu’il devait y avoir une meilleure façon, moins coûteuse et plus précieuse, de résoudre ces scénarios. Ainsi, l’idée d’utiliser des méthodes formelles pour créer des spécifications avant de mettre en œuvre le code a été créée. Alors, j’ai commencé mon parcours universitaire à cet égard, ce qui m’a menée à Informal Systems et à Quint.

Quint n’a pas été conçu à l’origine comme un produit. Nous l’avons construit par nécessité chez Informal Systems. Nous écrivions des spécifications TLA+ pour des systèmes dont nous avions besoin de faire confiance plus que nous ne le faisions, mais cela n’a pas dépassé un très petit groupe de personnes car la syntaxe était trop effrayante avec trop de symboles mathématiques, et les outils ne répondaient pas aux attentes de base des gens. Nous montrions à des collègues et à des collaborateurs externes : « regardez cette chose incroyable que j’ai faite », mais ils ne pouvaient pas la lire et n’avaient pas le temps d’apprendre un nouvel outil.

Les choix de conception dans Quint découlent directement de cette expérience. Le langage est facile à lire et à retenir. La première chose que nous avons construite était une extension VSCode qui met en évidence les erreurs au fur et à mesure que vous tapez. Il dispose de types et de modes distincts pour séparer explicitement les couches. Il dispose d’un REPL pour que vous puissiez explorer de manière interactive, et d’un simulateur pour que vous puissiez obtenir un retour rapide et itérer. Il exporte des traces vers un format JSON standardisé qui est facile à analyser pour les machines. Ceux-ci étaient des choses que les programmeurs attendaient déjà de leurs outils et que nous avions besoin nous-mêmes. La vérification sous-jacente est la même logique que TLA+.

Je suis obsédée par le fait de rendre les méthodes formelles plus accessibles, et la livraison d’outils est excitante, mais l’impact réel n’est ressenti que si les équipes d’ingénieurs les utilisent réellement. Il y a encore un delta entre ce que les outils peuvent faire et à quel point ils semblent utiles aux développeurs, et je travaille à combler cet écart.

Pour les lecteurs qui ne sont pas familiers avec cela, comment expliqueriez-vous ce qu’est Quint et pourquoi un nouveau langage de spécification était nécessaire aux côtés d’outils existants comme TLA+ ?

La plupart des spécifications sont de la documentation. Vous écrivez ce que le système devrait faire, et vous les vérifiez en les lisant. Le problème est que la documentation est incorrecte de manière que vous ne pouvez pas détecter mécaniquement : noms non définis, comportement ambigu, hypothèses implicites. Vous découvrez généralement cela pendant la mise en œuvre ou en production.

Une spécification Quint est quelque chose que vous exécutez. Vous modélisez le système comme une machine à états, définissez les propriétés qu’il devrait satisfaire, et exécutez ou vérifiez le modèle. S’il y a une violation, vous obtenez un contre-exemple montrant exactement la séquence d’étapes qui déclenche cela. Cela change lorsque et à quel point vous découvrez un défaut de conception à moindre coût.

TLA+ pouvait toujours le faire. Quint le rend pratique pour les ingénieurs qui ne sont pas déjà des spécialistes de la logique temporelle.

Quint est conçu pour combler le fossé entre les méthodes formelles et l’ingénierie logicielle quotidienne. Quels étaient les plus grands obstacles à l’utilisabilité que vous visiez à éliminer par rapport aux approches traditionnelles ?

Honnêtement, le plus grand obstacle à l’utilisabilité était la syntaxe. C’est pourquoi nous avons commencé par la syntaxe. Après avoir résolu cela, nous pouvions nous concentrer sur d’autres facteurs. Le système de types et d’effets de Quint est venu pour signaler autant d’erreurs que possible avant même de commencer le processus de vérification régulier, et les gens ont apprécié cela beaucoup. Cela nous a menés à écrire des spécifications de haute qualité que même plus de gens pouvaient lire. Nous l’avons intégré dans les éditeurs, et offert la fonctionnalité de base que tous les développeurs ont le droit d’attendre.

L’impact le plus important après cela a été notre simulateur. Il a commencé comme un moyen de fournir aux gens un premier retour sur le comportement de leur système, comme un développeur veut pouvoir exécuter le code après l’avoir écrit. Il s’est avéré être extrêmement précieux comme moyen d’obtenir confiance dans les spécifications qui sont trop grandes pour que la vérification puisse les gérer, puisque l’expertise pour adapter une spécification pour la rendre réalisable pour la vérification ne doit pas être tenue pour acquise. Notre simulateur a rendu la confiance plus accessible et nous l’avons utilisé de manière extensive dans de nombreux projets.

Mon plus grand point de douleur avec la syntaxe TLA+ était à quel point je mélangais souvent mes barres obliques inverses et mes barres obliques régulières, et vous devez taper celles-ci beaucoup. J’aime mieux la syntaxe de Quint, mais ce qui me rend vraiment impossible de revenir en arrière, c’est tous les outils.

L’une des forces de Quint est sa capacité à modéliser et à tester des systèmes distribués avant leur déploiement. Comment cela change la façon dont les ingénieurs devraient penser à la construction de systèmes comme les blockchains ou les infrastructures en temps réel ?

Le plus grand changement est le déplacement de la validation plus tôt. Leslie Lamport, le créateur de TLA+, compare l’écriture de spécifications avant le code à la création de plans avant les travaux de construction. Même si vous avez déjà construit quelque chose sans plan, il est encore une bonne idée de le créer maintenant et de l’utiliser pour éclairer vos changements futurs.

Dans l’industrie du logiciel, nous utilisons des fichiers markdown et des tableaux blancs. Peut-être pouvez-vous comparer cela à essayer de décrire textuellement un bâtiment. Cela fonctionne, mais sauriez-vous si les tailles des murs s’additionnent ? Quint offre un moyen de décrire des systèmes où vous pouvez être aussi haut niveau que vous le souhaitez, et obtenir des informations sur son comportement et sa correction.

Quint s’appuie sur les fondements de TLA+, qui est largement utilisé pour décrire les systèmes distribués. Comment avez-vous équilibré le maintien de cette rigueur théorique tout en rendant le langage plus convivial pour les développeurs ?

La décision clé a été de restreindre Quint à un fragment de TLA (la logique derrière TLA+) plutôt que d’exposer tout ce que la logique permet. TLA est très expressif, et une partie de cette expressivité inclut des opérateurs qui ne sont pas pris en charge par les outils, et permet des combinaisons que les gens comprennent et utilisent de manière incorrecte, ce qui rend les choses vraiment difficiles à déboguer. Nous avons pris une décision délibérée : nous nous en tenons à ce dont la plupart des spécifications réalistes ont réellement besoin, et nous évitons ce qui a un potentiel de confusion.

Le système de types et le système d’effets ajoutent des contraintes, mais des contraintes qui sont utiles. Ils empêchent une classe entière d’erreurs de spécification qui ne sont pas amusantes lorsqu’elles sont découvertes après que la vérification ait déjà démarré. Les types sont presque entièrement déduits et les effets sont cachés des utilisateurs, donc cela ajoute de la valeur sans friction.

Avant que j’apprenne l’existence de TLA+, j’ai effectué des travaux de recherche sur les systèmes de types, ce qui signifie que le vérificateur de types de Quint était probablement mon composant préféré à écrire. Je me souviens d’avoir bu un café à la saveur de Paçoca dans mes premiers mois chez Informal Systems pendant que je révisais un article sur le système de types et en pensant « ma vie est incroyable ».

Faire en sorte que le langage soit bon à utiliser tout en conservant la correspondance avec TLA+ (puisque les spécifications Quint peuvent être transcompilées en TLA+) a été un exercice de langage de programmation, et les discussions avec l’équipe ont été la ressource la plus utile, suivie des commentaires des premiers utilisateurs. Il y a encore des améliorations que nous voulons apporter, et cela pourrait être ma partie préférée du travail.

Vous avez également travaillé sur l’analyse statique et les systèmes de types. Comment ces expériences ont-elles influencé la vérification de types de Quint, l’outillage et l’expérience globale du développeur ?

La plus grande leçon que j’ai apprise dans ce monde est que tous les langages ne sont pas les mêmes. Vous entendrez des gens dire que c’est juste une question d’apprendre une nouvelle syntaxe, tous les mêmes concepts s’appliquent toujours, donc tous les langages sont égaux et c’est juste une question de goût. Ce n’est pas vrai. Le domaine des langages de programmation compte de grands chercheurs qui effectuent un travail incroyable pour faire avancer ce domaine, et ce n’est pas seulement pour rendre un langage plus joli ou plus à leur goût.

La programmation fonctionnelle m’a été présentée très tôt, j’ai appris Haskell en même temps que C (mon premier langage de programmation), et je suis très reconnaissante pour cela. C’est la fondation qui m’aide à voir que l’isolement des mutations d’état et de la non-déterminisme dans une couche mince dans Quint, et avoir toute la complexité dans des fonctions pures, aide objectivement dans de nombreux facteurs, et ce n’est pas seulement une question de goût. Je ne pense pas que la construction de Quint aurait été productive si les questions de goût étaient ouvertes à la discussion trop souvent.

En tant qu’enseignante de méthodes formelles, vous avez une perspective unique. Quels sont les malentendus les plus courants que les ingénieurs ont sur la vérification formelle aujourd’hui ?

Eh bien, j’enseignais à des étudiants de premier cycle qui venaient de commencer dans l’industrie. La grande majorité d’entre eux n’avaient jamais entendu parler de méthodes formelles ou de vérification formelle avant, donc pas de malentendus ! Le cursus a été conçu de telle sorte que la plupart d’entre eux n’ont pas non plus appris sur les systèmes distribués, et environ la moitié d’entre eux apprendraient sur les threads dans le même semestre. Je leur disais que je me sentais comme si j’enseignais ce qu’est un parapluie avant qu’ils n’aient jamais connu la pluie !

J’étais plus motivée à leur enseigner comment les méthodes formelles et la spécification formelle d’un système peuvent nous aider à raisonner sur les solutions et à trouver les cas limites que de leur faire penser qu’ils devraient vérifier formellement chaque logiciel qu’ils écriraient. Mon devoir final était un jeu de rôle sur table où différents ordres que les joueurs pouvaient prendre et différents paramètres devaient être pris en compte, en essayant d’imiter les difficultés que nous rencontrons dans les systèmes distribués autant que possible. Cela a réussi à être suffisamment difficile pour qu’ils aient besoin d’utiliser les outils pour trouver les cas limites et améliorer leurs solutions pour battre les monstres à la fin. J’espère qu’ils se souviendront de moi lorsque mereka seront confrontés à une situation similaire au travail un jour. Certains d’entre eux l’ont déjà fait.

Il y a un intérêt croissant pour combiner l’IA avec le développement de logiciels. Voyez-vous un rôle pour l’IA dans l’aide aux développeurs à écrire, valider ou même générer des spécifications formelles à l’aide d’outils comme Quint ?

Un rôle important, et cela se produit déjà. L’informatique est plus grande que l’écriture de code, et l’IA ouvre la porte à de nouvelles façons d’utiliser les méthodes formelles. Les LLM sont bons pour écrire des spécifications Quint à partir de descriptions de systèmes en langage naturel et même à partir de code existant. Le kit LLM de Quint comporte des agents de code Claude qui prennent une description anglaise d’un protocole et produisent une spécification Quint que vous pouvez exécuter et vérifier immédiatement.

Dans le même temps, Quint aide également les développeurs à faire confiance au code écrit avec l’IA. Je crois fortement que la confiance doit provenir de la compréhension, et non de quelques vérifications magiques. Travailler sur une spécification Quint qui conduit et vérifie le code d’implémentation signifie que les développeurs peuvent toujours posséder et comprendre le comportement du système, en résolvant la dette cognitive que l’utilisation de l’IA peut créer et en fournissant des moyens plus affirmatifs de valider le code généré.

Nous utilisons les LLM comme des outils de langage qui écrivent des définitions Quint précises à partir de l’intention du langage naturel, puis donnons les outils Quint à l’IA pour qu’elle puisse accomplir des choses qu’elle ne peut pas faire de manière fiable par elle-même, comme trouver les cas limites.

En regardant vers l’avenir, qu’est-ce qui doit se passer pour que les méthodes formelles passent d’une adoption de niche à une partie standard du cycle de vie du développement de logiciels ?

Depuis un certain temps, je sais que les deux choses de haut niveau dont Quint a besoin pour une adoption plus large sont un coût plus faible et une valeur plus élevée. Je pense que cela s’applique à beaucoup d’autres choses aussi. Les méthodes formelles viennent de recevoir un énorme coup de pouce dans ces deux choses, avec l’IA réduisant considérablement le coût d’écriture de spécifications formelles et créant également l’environnement de manque de confiance et de compréhension où les méthodes formelles peuvent avoir le plus d’impact et de valeur.

Avec l’IA changeant ce que notre profession est, au moins dans une certaine mesure, j’espère que ce changement est vers des choix de conception de niveau supérieur et la correction du comportement, faisant des méthodes formelles un outil de tous les jours ; et non vers le fait que nous ne comprenons plus aucun code ou système et que nous passons tout notre temps à examiner le code généré par l’IA sans aucun outil pour nous aider à raisonner à ce sujet.

Je vous remercie pour cet entretien éclairant ; les lecteurs intéressés pour en savoir plus sur ce langage de spécification exécutable pour la modélisation et la vérification de systèmes complexes, y compris son outillage et la façon de commencer, peuvent explorer Quint.