Gabriela Moreira, CEO di Quint presso Informal Systems – Intervista

Gabriela Moreira, CEO di Quint presso Informal Systems, è un’ingegnere di ricerca specializzata in linguaggi di programmazione e metodi formali, con un forte focus sulla creazione di strumenti che rendono la verifica dei sistemi complessi più accessibile agli ingegneri. Guida lo sviluppo di Quint, un linguaggio di specifica eseguibile moderno basato su TLA+, dove continua a mantenere e a far evolvere il linguaggio e la sua strumentazione. Il suo lavoro copre la verifica formale, l’analisi statica e la strumentazione per gli sviluppatori, e ha anche contribuito all’ambito accademico insegnando metodi formali, riflettendo una combinazione di ingegneria pratica e profondità teorica.

Quint, sviluppato e mantenuto presso Informal Systems, è un linguaggio di specifica moderno progettato per modellare, testare e verificare sistemi complessi come reti distribuite, blockchain e database. Costruito sulle fondamenta della Logica Temporale delle Azioni (TLA), Quint introduce una sintassi più amichevole per gli sviluppatori, insieme a strumenti avanzati come il controllo dei tipi, la simulazione e la verifica del modello, che consentono agli ingegneri di rilevare i fallimenti del sistema prima del deploy. La piattaforma enfatizza le specifiche eseguibili, consentendo agli sviluppatori non solo di descrivere il comportamento del sistema, ma anche di testarlo e esplorarlo attivamente, colmando il divario tra la correttezza teorica e l’implementazione nel mondo reale.

Ritornando all’inizio, cosa ha innescato il tuo interesse per la programmazione, e come hai finito per entrare nel campo dei metodi formali e dei sistemi distribuiti?

Ero un’avidissima giocatrice con un computer scadente, e mi resi conto che mi piaceva risolvere i problemi e farlo funzionare. Mi iscrissi a scienze informatiche e fui attratta dalla teoria e dai compilatori.

Nel 2015, mi sono imbattuta in concorsi di programmazione. In quelli, di solito si ottengono alcuni esempi di input e output attesi, e si scrive il codice che risolve il problema e funziona per quegli esempi. Tuttavia, dopo averlo inviato per la valutazione, il codice viene effettivamente testato con molti più esempi oltre quelli che vengono mostrati. Quella consapevolezza che il codice potrebbe funzionare per gli scenari che vedo o penso, ma potrebbe comunque fallire in casi che non ho considerato, ha reso la programmazione una sorta di sfida di cui mi sono innamorata.

Lavorando nell’industria, fui rapidamente attratta dai sistemi distribuiti, dove dovevamo considerare diversi ordini in cui i messaggi potevano arrivare, diversi modi di fallimento e un intero mondo di comportamenti nascosti. Nel 2018, un collega mi ha presentato un linguaggio di specifica formale chiamato TLA+. Ne sono rimasta affascinata. Ho immediatamente iniziato a costruire strumenti intorno a TLA+ e ho lavorato in questo settore da allora.

Hai costruito la tua carriera intorno ai metodi formali e ai linguaggi di programmazione, dal tuo lavoro iniziale sugli strumenti basati sulla Logica Temporale delle Azioni (TLA+) alla guida dello sviluppo di Quint presso Informal Systems. Cosa ti ha motivato a concentrarti sul rendere la verifica formale più accessibile, e come ha plasmato il design di Quint?

TLA+ è troppo buono per non essere utilizzato ampiamente nell’industria. Ero ancora abbastanza giovane quando ho imparato a conoscerlo, e mi univo a queste chiamate con i miei colleghi di lavoro per cercare di trovare soluzioni insieme, e costantemente trovavo scenari in cui le nostre soluzioni avrebbero fallito. Tuttavia, ero sempre l’ultima linea di difesa contro quegli scenari nella maggior parte dei casi. Mi resi conto che doveva esserci un modo migliore, meno costoso e più prezioso per risolvere quegli scenari. Così, l’idea di utilizzare metodi formali per creare specifiche prima di implementare il codice è stata creata. Quindi, ho iniziato il mio percorso accademico verso di esso, che mi ha portato a Informal Systems e a Quint.

Quint non è stato originariamente concepito come un prodotto. L’abbiamo costruito per necessità presso Informal Systems. Stavamo scrivendo specifiche TLA+ per sistemi di cui avevamo bisogno di fidarci più di quanto facessimo, ma che non si espandevano oltre un piccolo gruppo di persone poiché la sintassi era troppo spaventosa con troppi simboli matematici, e la strumentazione non soddisfaceva le aspettative di base delle persone. Mostravamo ai colleghi e ai collaboratori esterni: “guardate questa cosa incredibile che ho fatto”, ma non potevano leggerla e non avevano il tempo di imparare uno strumento nuovo.

Le scelte di design in Quint derivano direttamente da quell’esperienza. Il linguaggio è facile da leggere e ricordare. La prima cosa che abbiamo costruito è stata un’estensione VSCode che evidenzia gli errori mentre si digita. Ha tipi e modalità distinte per separare esplicitamente i livelli. Ha un REPL in modo che si possa esplorare interattivamente, e un simulatore in modo che si possa ottenere un feedback rapido e iterare. Esporta tracce in un formato JSON standardizzato che è facile da analizzare per le macchine. Queste erano cose che i programmatori già si aspettavano dai loro strumenti e che anche noi avevamo bisogno di avere. La verifica sottostante è la stessa logica di TLA+.

Sono ossessionata dal rendere i metodi formali più accessibili, e spedire strumenti è emozionante, ma l’impatto reale si avverte solo se i team di ingegneria li utilizzano effettivamente. C’è ancora un delta tra ciò che gli strumenti possono fare e quanto utili sembrano agli sviluppatori, e sto lavorando per colmare quel divario.

Per i lettori che non conoscono Quint, come spiegheresti cosa è e perché è necessario un nuovo linguaggio di specifica accanto a strumenti esistenti come TLA+?

La maggior parte delle specifiche sono documentazione. Si scrive cosa il sistema dovrebbe fare e si controlla leggendo. Il problema è che la documentazione è sbagliata in modi che non possono essere rilevati meccanicamente: nomi non definiti, comportamento ambiguo, assunzioni implicite. Di solito si scopre durante l’implementazione o in produzione.

Una specifica Quint è qualcosa che si esegue. Si modella il sistema come una macchina a stati, si definiscono le proprietà che deve soddisfare e si esegue o si verifica il modello. Se c’è una violazione, si ottiene un controesempio che mostra esattamente la sequenza di passaggi che la scatena. Ciò cambia quando e come rileviamo un difetto di progettazione.

TLA+ poteva già farlo. Quint lo rende pratico per gli ingegneri che non sono già specialisti in logica temporale.

Quint è progettato per colmare il divario tra metodi formali e ingegneria del software quotidiana. Quali sono stati i più grandi ostacoli all’usabilità che hai cercato di eliminare rispetto agli approcci tradizionali?

Onestamente, l’ostacolo più grande è stata la sintassi. È per questo che abbiamo iniziato con la sintassi. Dopo aver affrontato questo, abbiamo potuto concentrarci su altri fattori. Il sistema di tipi e di effetti di Quint è arrivato per segnalare il maggior numero possibile di errori prima di iniziare il processo di verifica regolare, e le persone lo hanno molto apprezzato. Ciò ci ha portato a scrivere specifiche di alta qualità che anche più persone potevano leggere. Le abbiamo integrate negli editor e offerto la funzionalità di base che tutti gli sviluppatori hanno il diritto di aspettarsi.

L’impatto più grande dopo di quello è stato il nostro simulatore. È iniziato come un modo per offrire alle persone un feedback iniziale sul comportamento del loro sistema, come uno sviluppatore vuole essere in grado di eseguire il codice dopo averlo scritto. È poi risultato estremamente prezioso come un modo per ottenere fiducia nelle specifiche che sono troppo grandi per la verifica da gestire, poiché l’esperienza di adattare una specifica per renderla fattibile per la verifica non dovrebbe essere data per scontata. Il nostro simulatore ha reso la fiducia più accessibile e l’abbiamo utilizzato ampiamente in molti progetti.

Il mio più grande punto dolente con la sintassi TLA+ era quanto frequentemente confondevo le mie barre rovesce e le barre normali, e dovevo digitarle molto. Mi piace la sintassi di Quint molto di più, ma ciò che mi rende impossibile tornare indietro è tutta la strumentazione.

Una delle forze di Quint è la sua capacità di modellare e testare sistemi distribuiti prima del deploy. Come ciò cambia il modo in cui gli ingegneri dovrebbero pensare alla costruzione di sistemi come blockchain o infrastrutture in tempo reale?

Il più grande cambiamento è spostare la convalida più presto. Leslie Lamport, creatore di TLA+, paragona la scrittura di specifiche prima del codice a disegnare progetti prima dei lavori di costruzione. Anche se hai già costruito qualcosa senza un progetto, è ancora una buona idea scriverlo adesso e utilizzarlo per informare i tuoi cambiamenti futuri.

Nell’industria del software, utilizziamo file markdown e lavagne. Forse puoi paragonarlo a cercare di descrivere testualmente un edificio. Funziona, ma sapresti se le dimensioni dei muri si sommano? Quint offre un modo per descrivere sistemi in cui puoi essere alto livello quanto vuoi e ottenere informazioni sul suo comportamento e sulla sua correttezza.

Quint si basa sulle fondamenta di TLA+, ampiamente utilizzato per descrivere sistemi distribuiti. Come hai bilanciato il mantenimento di quella rigorosità teorica mentre rendevi il linguaggio più amichevole per gli sviluppatori?

La decisione chiave è stata limitare Quint a un frammento di TLA (la logica dietro TLA+) piuttosto che esporre tutto ciò che la logica consente. TLA è molto espressivo, e parte di quell’espressività include operatori che non sono supportati da alcuno strumento e permette combinazioni che le persone capiscono e utilizzano in modo errato, rendendo le cose molto difficili da debuggare. Abbiamo preso una decisione deliberata: attenersi a ciò che la maggior parte delle specifiche realistiche effettivamente necessita e evitare ciò che ha il potenziale per la confusione.

Il sistema di tipi ed effetti aggiunge vincoli, ma vincoli che sono utili. Impediscono una classe intera di errori di specifica che non sono divertenti quando vengono trovati dopo che la verifica è già in esecuzione. I tipi sono quasi interamente dedotti e gli effetti sono nascosti agli utenti, quindi questo aggiunge valore senza attrito.

Prima di conoscere l’esistenza di TLA+, stavo facendo ricerca su sistemi di tipi, il che significa che il controllo dei tipi di Quint è stato probabilmente il mio componente preferito da scrivere. Ricordo di aver bevuto un caffè al gusto di Paçoca nei miei primi mesi a Informal mentre esaminavo un documento sul sistema di tipi e pensavo “la mia vita è incredibile”.

Rendere il linguaggio buono da usare mentre manteneva la corrispondenza con TLA+ (poiché le specifiche Quint possono essere trasformate in TLA+) è stato un esercizio di linguaggio di programmazione, e le discussioni con il team sono state la risorsa più utile, seguite dal feedback degli utenti precoci. Ci sono ancora miglioramenti che vogliamo fare, e potrebbe essere la mia parte preferita del lavoro.

Hai anche lavorato sull’analisi statica e sui sistemi di tipi. Come queste esperienze hanno influenzato il controllo dei tipi di Quint, la strumentazione e l’esperienza complessiva degli sviluppatori?

La più grande lezione che ho imparato in quel mondo è che non tutti i linguaggi sono uguali. Sentirai persone dire che è solo questione di imparare una nuova sintassi, tutti gli stessi concetti si applicano ancora, quindi tutti i linguaggi sono uguali e si tratta solo di gusto. Non è vero. Il campo dei linguaggi di programmazione ha grandi ricercatori che fanno lavori incredibili per far avanzare questo campo, e che non è solo per fare in modo che un linguaggio appaia più bello o più di loro gradimento.

La programmazione funzionale mi è stata presentata molto presto, ho imparato Haskell allo stesso tempo in cui ho imparato C (il mio primo linguaggio di programmazione), e sono molto grata per questo. Questo è il fondamento che mi aiuta a vedere che isolare le mutazioni dello stato e la non determinismo in uno strato sottile in Quint, e avere tutta la complessità in funzioni pure, aiuta obiettivamente in molti fattori, e non è solo questione di gusto. Non credo che costruire Quint sarebbe stato produttivo se le questioni di gusto fossero state soggette a discussione troppo spesso.

Insegnare metodi formali come docente ti dà una prospettiva unica. Quali sono i più comuni malintesi che gli ingegneri hanno sui metodi di verifica formale oggi?

Beh, stavo insegnando a studenti universitari che stavano solo iniziando a entrare nel settore. La stragrande maggioranza di loro non aveva mai sentito parlare di metodi formali o di verifica formale prima, quindi nessun malinteso! Il curriculum era stato progettato in modo che la maggior parte di loro non avesse anche imparato sui sistemi distribuiti, e circa la metà di loro avrebbe imparato sui thread nello stesso semestre. Mi piaceva dire loro che mi sentivo come se stessi insegnando loro cosa sia un ombrello e a cosa serva prima che avessero mai sperimentato la pioggia!

Ero più motivata a insegnare loro come i metodi formali e la specifica formale di un sistema possano aiutarci a ragionare sulle soluzioni e trovare casi limite piuttosto che far loro pensare che dovrebbero verificare formalmente ogni software che scrivono. Il mio compito finale era un setup di gioco da tavolo in cui diversi ordini che i giocatori potevano eseguire e diversi setup dovevano essere presi in considerazione, cercando di mimare le difficoltà che affrontiamo nei sistemi distribuiti il più possibile. È riuscito a essere abbastanza difficile da far sì che loro dovessero utilizzare gli strumenti per trovare casi limite e migliorare le loro soluzioni per sconfiggere i mostri alla fine. Spero che quando si troveranno ad affrontare una situazione simile al lavoro un giorno, si ricorderanno di me. Alcuni di loro già lo hanno fatto.

C’è un crescente interesse per la combinazione dell’intelligenza artificiale con lo sviluppo del software. Vedi un ruolo per l’intelligenza artificiale nell’aiutare gli sviluppatori a scrivere, convalidare o anche generare specifiche formali utilizzando strumenti come Quint?

Un ruolo significativo, e già sta accadendo. La scienza informatica è più grande della scrittura del codice, e l’intelligenza artificiale apre la porta a modi completamente nuovi di utilizzare metodi formali. I LLM sono bravi a scrivere specifiche Quint da descrizioni linguistiche naturali di un sistema e anche da codice esistente. Il kit LLM di Quint ha agenti di codice Claude che prendono una descrizione inglese di un protocollo e producono una specifica Quint che puoi eseguire e controllare immediatamente.

Allo stesso tempo, Quint aiuta anche gli sviluppatori a fidarsi del codice scritto con l’intelligenza artificiale. Credo fortemente che la fiducia debba venire dalla comprensione, non da qualche controllo magico. Lavorare su una specifica Quint che guida e controlla il codice di implementazione significa che gli sviluppatori possono ancora possedere e capire il comportamento del sistema, affrontando il debito cognitivo che l’uso dell’intelligenza artificiale può creare e fornendo modi più assertivi di convalidare il codice generato.

Sfruttiamo i LLM come strumenti linguistici che scrivono definizioni precise di Quint da intenti linguistici naturali, e poi diamo gli strumenti di Quint all’intelligenza artificiale in modo che possa realizzare cose che non può fare in modo affidabile da sola, come trovare casi limite.

Guardando avanti, cosa deve accadere perché i metodi formali passino dall’adozione di nicchia a una parte standard del ciclo di vita dello sviluppo del software?

Da un po’ di tempo so che le due cose principali di cui Quint ha bisogno per un’adozione più ampia sono: costo più basso e valore più alto. Credo che questo si applichi a molte altre cose. I metodi formali hanno appena ricevuto un grande impulso in entrambi questi aspetti, con l’intelligenza artificiale che riduce notevolmente il costo di scrittura delle specifiche formali e crea anche l’ambiente di mancanza di fiducia e comprensione in cui i metodi formali possono essere più impattanti e preziosi.

Con l’intelligenza artificiale che cambia cosa è la nostra professione, almeno in una certa misura, spero che questo cambiamento sia verso scelte di design di alto livello e correttezza del comportamento, rendendo i metodi formali uno strumento quotidiano; e non verso il fatto che non capiamo più alcun codice o sistema e passiamo tutto il nostro tempo a esaminare il codice generato dall’intelligenza artificiale senza alcuno strumento per aiutarci a ragionare su di esso.

Grazie per l’intervista approfondita; i lettori interessati a saperne di più su questo linguaggio di specifica eseguibile per la modellazione e la verifica di sistemi complessi, compresa la sua strumentazione e come iniziare, possono esplorare Quint.