Gabriela Moreira, CEO al Quint la Informal Systems – Seria de interviuri

Gabriela Moreira, CEO al Quint la Informal Systems, este un inginer de cercetare specializat în limbaje de programare și metode formale, cu un accent puternic pe construirea unor instrumente care fac verificarea sistemelor complexe mai accesibilă inginerilor. Ea conduce dezvoltarea Quint, o limbaj modern de specificație executabilă bazat pe TLA+, unde continuă să mențină și să evolueze limbajul și instrumentele sale. Activitatea sa se extinde asupra verificării formale, analizei statice și instrumentelor pentru dezvoltatori, iar ea a contribuit și la academia, predând metode formale, reflectând o combinație de inginerie practică și profunzime teoretică.

Quint, dezvoltat și întreținut la Informal Systems, este un limbaj modern de specificație proiectat pentru a modela, testa și verifica sisteme complexe, cum ar fi rețele distribuite, blockchain și baze de date. Construit pe fundațiile Logicii Temporale a Acțiunilor (TLA), Quint introduce o sintaxă mai prietenoasă pentru dezvoltatori, împreună cu instrumente avansate, cum ar fi verificarea de tip, simularea și verificarea modelului, care permit inginerilor să detecteze defectele sistemului înainte de implementare. Platforma pune accentul pe specificații executabile, permițând dezvoltatorilor nu numai să descrie comportamentul sistemului, ci și să îl testeze și să îl exploreze activ, reducând decalajul dintre corectitudinea teoretică și implementarea din lumea reală.

Întorcându-ne la început, ce a declanșat inițial interesul dvs. pentru programare, și cum ați ajuns să vă implicați în metode formale și sisteme distribuite?

Eram un jucător înrăit cu un calculator slab, și am realizat că îmi place să repar problemele și să îl fac să funcționeze. M-am înscris la știința calculatoarelor și am fost atras de teorie și compilatoare. 

În 2015, am participat la concursuri de programare. În acestea, de obicei, primiți câteva exemple de intrare și ieșire așteptată, și scrieți cod care rezolvă problema și funcționează pentru acele exemple. Cu toate acestea, după ce îl trimiteți pentru evaluare, codul este de fapt testat cu mult mai multe exemple dincolo de cele pe care le-ați văzut. Acea realizare că codul poate funcționa pentru scenariile pe care le văd sau le imaginez, dar poate eşua în cazuri pe care nu le-am luat în considerare, a transformat programarea într-un fel de provocare de care m-am îndrăgostit.

Lucrând în industrie, am fost atras rapid de sistemele distribuite, unde trebuia să luăm în considerare diferite ordonări ale mesajelor care pot ajunge, diferite moduri de eșec și un întreg univers de comportamente ascunse. În 2018, un coleg mi-a prezentat un limbaj de specificație formală numit TLA+. Am fost capturat. Am început imediat să construiesc instrumente în jurul TLA+ și am lucrat în acest domeniu de atunci.

Ați construit cariera în jurul metodelor formale și limbajelor de programare, de la munca dvs. timpurie pe instrumente bazate pe Logica Temporală a Acțiunilor (TLA+) la conducerea dezvoltării Quint la Informal Systems. Ce v-a motivat să vă concentrați pe facerea verificării formale mai accesibilă, și cum a influențat această viziune designul Quint?

TLA+ este prea bun pentru a nu fi utilizat pe scară largă în industrie. Eram încă destul de tânăr când am aflat despre el, și mă alăturam apelurilor cu colegii mei de muncă pentru a încerca să găsim soluții împreună, și mereu găseam scenarii în care soluțiile noastre ar fi eșuat. Cu toate acestea, eram întotdeauna ultima linie de apărare împotriva acestor scenarii în majoritatea cazurilor. Am considerat că trebuie să existe o modalitate mai bună, mai puțin costisitoare și mai valoroasă de a rezolva aceste scenarii. Astfel, ideea de a utiliza metode formale pentru a crea specificații înainte de implementarea codului a fost creată. Așa că am început drumul meu academic spre acest scop, ceea ce m-a condus la Informal Systems și Quint.

Quint nu a fost conceput inițial ca un produs. L-am construit din necesitate la Informal Systems. Scriam specificații TLA+ pentru sisteme pe care trebuia să le încredințăm mai mult decât făceam, dar care nu s-au extins dincolo de un grup foarte mic de oameni, deoarece sintaxa era prea înfricoșătoare, cu prea multe simboluri matematice, și instrumentele nu au îndeplinit așteptările oamenilor. Le-arătam colegilor și colaboratorilor externi: „uitați-vă la această minunată chestie pe care am făcut-o”, dar ei nu puteau să o citească și nu aveau timp să învețe un instrument nou.

Alegerea designului în Quint urmează direct din această experiență. Limbajul este ușor de citit și de reținut. Prima lucrare pe care am construit-o a fost o extensie VSCode care evidențiază erorile pe măsură ce le tastați. Are tipuri și moduri distincte pentru a separa straturile în mod explicit. Are un REPL pentru a explora interactiv și un simulator pentru a obține feedback rapid și a itera. Exportă urme într-un format JSON standardizat, care este ușor de parsat de mașini. Acestea erau lucruri pe care programatorii le așteptau deja de la instrumentele lor și pe care le-am necesitat și noi. Verificarea de sub este aceeași logică ca TLA+.

Sunt obsedat de a face metodele formale mai accesibile, și lansarea instrumentelor este emocionantă, dar impactul real se resimte doar dacă echipele de ingineri le folosesc cu adevărat. Există încă un decalaj între ceea ce pot face instrumentele și cât de utile li se par dezvoltatorilor, și lucrez pentru a închide acest decalaj.

Pentru cititorii care nu sunt familiari cu el, cum ați explica ce este Quint și de ce a fost nevoie de un nou limbaj de specificație lângă instrumente existente, cum ar fi TLA+?

Majoritatea specificațiilor sunt documentație. Scrieți ce ar trebui să facă sistemul și le verificați citindu-le. Problema este că documentația este greșită în moduri pe care nu le puteți detecta mecanic: nume nedeterminate, comportament ambiguu, ipoteze implicite. De obicei, aflați despre asta în timpul implementării sau în producție.

O specificație Quint este ceva pe care îl executați. Modelați sistemul ca o mașină de stare, definiți proprietățile pe care ar trebui să le îndeplinească și rulați sau verificați modelul. Dacă există o încălcare, primiți un exemplu care arată exact secvența de pași care declanșează aceasta. Acest lucru schimbă momentul și modul în care prindeți o eroare de proiectare.

TLA+ putea face asta întotdeauna. Quint face ca acest lucru să fie practic pentru ingineri care nu sunt deja specialiști în logică temporală.

Quint este proiectat pentru a reduce decalajul dintre metodele formale și ingineria software de zi cu zi. Care au fost cele mai mari bariere de utilizare pe care ați încercat să le eliminați în comparație cu abordările tradiționale?

Sincer, cea mai mare barieră de utilizare a fost sintaxa. De aceea am început cu sintaxa. După ce am abordat acest aspect, am putut să ne concentrăm mai mult pe alți factori. Sistemul de tip și efect al lui Quint a venit să semnaleze cât mai multe erori posibile înainte de a începe procesul de verificare regulat, și oamenii au apreciat foarte mult asta. Ne-a condus să scriem specificații de calitate superioară pe care și mai mulți oameni le puteau citi. Le-am integrat în editoare și am oferit funcționalitatea de bază pe care toți dezvoltatorii o așteaptă.

Impactul cel mai mare după aceea a fost simulatorul nostru. A început ca o modalitate de a oferi oamenilor un feedback inițial despre comportamentul sistemului lor, așa cum dorește un dezvoltator să poată, cumva, să ruleze codul după ce l-a scris. Așa că a devenit extrem de valoros ca modalitate de a obține încredere în specificații care sunt prea mari pentru a fi verificate, deoarece expertiza de a adapta o specificație pentru a o face fezabilă pentru verificare nu ar trebui să fie luată de bună. Simulatorul nostru a făcut ca încrederea să fie mai accesibilă, și l-am folosit pe scară largă în multe proiecte.

Punctul meu de durere cu sintaxa TLA+ a fost cât de des am amestecat backslash-urile și slash-urile normale, și trebuie să tastez multe astfel de caractere. Îmi place sintaxa lui Quint mult mai bine, dar ceea ce mă face să nu pot reveni la TLA+ este întregul instrumentar.

Una dintre puterile lui Quint este capacitatea sa de a modela și testa sisteme distribuite înainte de implementare. Cum schimbă acest lucru modul în care inginerii ar trebui să gândească despre construirea sistemelor, cum ar fi blockchain sau infrastructura în timp real?

Schimbarea cea mai mare este mutarea validării mai devreme. Leslie Lamport, creatorul TLA+, compară scrierea de specificații înainte de cod cu desenarea de planuri înainte de lucrările de construcție. Chiar dacă ați construit deja ceva fără un plan, este încă o idee bună să scrieți unul acum și să îl folosiți pentru a informa modificările ulterioare.

În industria software, folosim fișiere markdown și table. Poate că puteți compara asta cu încercarea de a descrie textual o clădire. Funcționează, dar ați ști dacă dimensiunile pereților se adună? Quint oferă o modalitate de a descrie sisteme în care puteți fi la nivelul dorit și obțineți informații despre comportamentul și corectitudinea sa.

Quint se bazează pe fundațiile TLA+, care este utilizat pe scară largă pentru a descrie sisteme distribuite. Cum ați echilibrat menținerea acestei rigori teoretice, în timp ce faceți limbajul mai prietenos pentru dezvoltatori?

Decizia cheie a fost să restricționați Quint la o parte a TLA (logica din spatele TLA+) și nu să expuneți tot ceea ce permite logica. TLA este foarte expresiv, și o parte din această expresivitate include operatori care nu sunt suportați de niciun instrument și permite combinații pe care oamenii le înțeleg și le folosesc greșit, făcând foarte dificilă depistarea erorilor. Am făcut o alegere deliberată: să ne limităm la ceea ce specițiile realiste necesită în mod normal și să evităm ceea ce are potențial de a crea confuzie.

Sistemul de tip și efect adaugă constrângeri, dar constrângeri care sunt utile. Ele previn o întreagă clasă de erori de specificație care nu sunt plăcute atunci când sunt descoperite după ce verificarea a început deja. Tipurile sunt aproape în întregime inferate, iar efectele sunt ascunse de la utilizatori, astfel încât adaugă valoare fără nicio fricțiune.

Înainte de a afla despre existența TLA+, făceam cercetare în sisteme de tip, ceea ce înseamnă că verificatorul de tip al lui Quint a fost probabil componenta mea preferată de scris. Îmi amintesc că beam o cafea cu aroma Paçoca în primele mele luni la Informal, în timp ce revădeam o lucrare despre sisteme de tip și gândeam „viața mea este minunată”. 

Făcând limbajul bun de utilizat, în timp ce păstram corespondența cu TLA+ (deoarece specițiile Quint pot fi transpuse în TLA+), a fost un exercițiu de limbaj de programare, iar discuțiile cu echipa au fost cel mai util resurs, urmat de feedback-ul de la utilizatorii timpurii. Există încă îmbunătățiri pe care le dorim, și poate că este partea mea preferată a jobului.

Ați lucrat și la analiză statică și sisteme de tip. Cum au influențat aceste experiențe verificarea de tip a lui Quint, instrumentarul și experiența generală a dezvoltatorului?

Lecția cea mai importantă pe care am învățat-o în acel domeniu este că nu toate limbajele sunt la fel. Veți auzi oameni spunând că este doar o chestiune de a învăța o nouă sintaxă, toate conceptele rămân aceleași, deci toate limbajele sunt egale și este doar o chestiune de gust. Acest lucru nu este adevărat. Domeniul limbajelor de programare are cercetători remarcabili care fac o muncă extraordinară pentru a avansa acest domeniu, și aceasta nu este doar pentru a face un limbaj să arate mai frumos sau mai plăcut.

Programarea funcțională mi-a fost prezentată foarte devreme, am învățat Haskell în același timp cu C (prima mea limbă de programare), și sunt foarte recunoscător pentru asta. Aceasta este fundația care mă ajută să văd că izolarea mutațiilor de stare și a non-determinismului într-un strat subțire în Quint, și având toată complexitatea în funcții pure, ajută obiectiv în multe aspecte, și nu este doar o chestiune de gust. Nu cred că construirea lui Quint ar fi fost productivă dacă chestiunile de gust ar fi fost supuse discuției prea des.

Învățarea metodelor formale ca lector vă oferă o perspectivă unică. Care sunt cele mai comune concepții greșite pe care inginerii le au despre verificarea formală în prezent?

Ei bine, predam studenților de la ciclul universitar care abia începeau în industrie. Majoritatea lor nu auziseră niciodată despre metode formale sau verificare formală înainte, deci nu existau concepții greșite! Curriculumul a fost făcut astfel încât majoritatea lor nici măcar nu învățaseră despre sisteme distribuite, și jumătate dintre ei urmau să învețe despre fire în același semestru. Le spuneam că mă simțeam ca și cum aș fi învățat ce este o umbrelă bună pentru ei înainte de a fi experimentat vreo ploaie!

Eram mai motivat să îi învăț cum metodele formale și specificarea formală a unui sistem pot ajuta la găsirea soluțiilor și a cazurilor limită, decât să îi fac să creadă că ar trebui să verifice formal orice software pe care îl scriu. Tema mea finală a fost o configurație de joc de rol pe masă, unde ordinea pe care jucătorii o puteau lua și configurațiile diferite trebuiau luate în considerare, încercând să imite dificultățile pe care le întâlnim în sisteme distribuite cât mai mult posibil. A reușit să fie suficient de dificilă, astfel încât ei au trebuit să folosească instrumentele pentru a găsi cazuri limită și a-și îmbunătăți soluțiile pentru a învinge monștrii la final. Sper că, atunci când se vor confrunta cu o situație similară la serviciu, își vor aminti de mine. Unii dintre ei deja au făcut-o.

Există un interes crescând în a combina inteligența artificială cu dezvoltarea software. Vezi un rol pentru inteligența artificială în a ajuta dezvoltatorii să scrie, să valideze sau chiar să genereze specificații formale, folosind instrumente precum Quint?

Unul semnificativ, și acesta se întâmplă deja. Informatica este mai mare decât scrierea de cod, și inteligența artificială deschide ușa către modalități complet noi de a utiliza metode formale. LLM-urile sunt bune la scrierea de specificații Quint din descrieri de limbaj natural ale unui sistem și chiar din cod existent. Kit-ul LLM Quint are agenți Claude Code care iau o descriere în engleză a unui protocol și produc o specificație Quint pe care o puteți rula și verificați imediat.

În același timp, Quint ajută și la încrederea în codul scris cu inteligență artificială. Cred cu tărie că încrederea trebuie să vină din înțelegere, nu de la vreo verificare magică. Lucrul la o specificație Quint care conduce și verifică codul de implementare înseamnă că dezvoltatorii pot încă deține și înțelege comportamentul sistemului, abordând datoria cognitivă pe care utilizarea inteligenței artificiale o poate crea și oferind modalități mai asertive de validare a codului generat.

Utilizăm LLM-uri ca instrumente de limbaj care scriu definiții precise Quint din intenția de limbaj natural, și apoi dăm instrumentele Quint inteligenței artificiale, astfel încât aceasta să poată realiza lucruri pe care nu le poate face în mod fiabil singură, cum ar fi găsirea de cazuri limită.

Privind înainte, ce trebuie să se întâmple pentru ca metodele formale să treacă de la adoptarea de nișă la a deveni o parte standard a ciclului de viață al dezvoltării software?

De ceva timp, știu că cele două lucruri de nivel înalt pe care Quint are nevoie pentru o adoptare mai mare sunt costul mai mic și valoarea mai mare. Cred că acest lucru se aplică și altor lucruri. Metodele formale au primit recent un impuls mare atât în ceea ce privește costul, cât și valoarea, odată cu inteligența artificială reducând semnificativ costul scrierii de specificații formale și creând, de asemenea, un mediu în care lipsa de încredere și înțelegere face ca metodele formale să fie cel mai impact și valoros.

Cu inteligența artificială schimbând ceea ce este profesiunea noastră, cel puțin într-o oarecare măsură, sper că această schimbare se îndreaptă către decizii de proiectare de nivel superior și corectitudine a comportamentului, făcând metodele formale un instrument de zi cu zi; și nu către a nu mai înțelege niciun cod sau sisteme și a petrece tot timpul nostru revizuind cod generat de inteligența artificială fără niciun instrumentar care să ne ajute să raționăm despre el.

Mulțumim pentru interviul plin de insight; cititorii interesați să afle mai multe despre acest limbaj de specificație executabilă pentru modelarea și verificarea sistemelor complexe, inclusiv instrumentarul și modul de a începe, pot explora Quint.