Gabriela Moreira, Quintin toimitusjohtaja Informal Systemsissa – Haastattelusarja

Gabriela Moreira, Quintin toimitusjohtaja Informal Systemsissa, on tutkimusinsinööri, joka on erikoistunut ohjelmointikieliin ja formaaleihin menetelmiin, ja hänellä on vahva painopiste kehittää työkaluja, jotka tekevät monimutkaisen järjestelmän verifioinnin helpommaksi insinööreille. Hän johtaa Quintin kehitystä, joka on moderni suoritettava määrityskieli, joka perustuu TLA+:aan, ja hän jatkaa kielen ja sen työkalujen ylläpitämistä ja kehittämistä. Hänen työnsä kattaa formaalisen verifioinnin, staattisen analyysin ja kehittäjien työkalut, ja hän on myös osallistunut akateemiseen yhteisöön opettamalla formaaleja menetelmiä, mikä heijastaa sekä käytännön insinööritaitoa että teoreettista syvyyttä.

Quint, jota kehitetään ja ylläpidetään Informal Systemsissa, on moderni määrityskieli, joka on suunniteltu monimutkaisten järjestelmien, kuten hajautettujen verkkojen, blockchainien ja tietokantojen, mallintamiseen, testaamiseen ja verifioimiseen. Se perustuu Temporal Logic of Actions (TLA) -periaatteisiin, ja Quint esittelee kehittäjien kannalta ystävällisemmän syntaksin, sekä edistyneen työkalujen, kuten tyyppitarkistuksen, simulaation ja mallin verifioinnin, jolloin insinöörit voivat havaita järjestelmän virheitä ennen käyttöönottoa. Alusta korostaa suoritettavia määrityksiä, mikä mahdollistaa kehittäjien kuvailla järjestelmän käyttäytymistä ja aktiivisesti testata ja tutkia sitä, mikä siltaa teoreettisen oikeellisuuden ja todellisen toteutuksen välisen kuilun.

Mennään alkuun, mitä ensin herätti sinussa kiinnostuksen ohjelmointiin, ja miten päädyit lopulta formaaleihin menetelmiin ja hajautettuihin järjestelmiin?

Olin innokas pelaaja, jolla oli huono tietokone, ja tajusin, että nautin ongelmien korjaamisesta ja saamisesta toimimaan. Kirjauduin tietojenkäsittelytieteen kursseille ja kiinnostuin teoriasta ja kääntäjistä.

Vuonna 2015 minut esiteltiin ohjelmointikilpailuun. Niissä saat useita esimerkkejä syötetestauksesta ja odotetusta tuloksesta, ja kirjoitat koodin, joka ratkaisee ongelman ja toimii näille esimerkeille. Mutta kun lähetät sen arvioitavaksi, koodi testataan monilla muilla esimerkeillä, joita et välttämättä ole ajatellut. Tämä tajunta, että koodi saattaa toimia skenaarioissa, joita näen tai ajattelen, mutta voi epäonnistua tapauksissa, joita en ole ajatellut, muutti ohjelmoinnin haasteeksi, johon rakastuin.

Teollisuudessa työskennellessäni kiinnostuin nopeasti hajautettuihin järjestelmiin, joissa meidän piti ottaa huomioon eri järjestykset, joissa viestit saapuvat, eri virhetilanteita ja piileviä käyttäytymisiä. Vuonna 2018 kollegani esitteli minulle formaalisen määrityskielen nimeltä TLA+. Olin koukussa. Aloin välittömästi kehittää työkaluja TLA+:n ympärille ja olen työskennellyt tässä alassa siitä lähtien.

Olet rakentanut urasi formaalisten menetelmien ja ohjelmointikielten ympärille, alkuvaiheista työstä TLA+:n pohjalta kehittäen Quintin Informal Systemsissa. Mitä motivoi sinua keskittymään formaalisen verifioinnin tekemiseen helpommaksi, ja miten tämä visio on muovannut Quintin suunnittelua?

TLA+ on liian hyvä, jotta se ei olisi laajasti käytössä teollisuudessa. Olin vielä melko nuori, kun opin siitä, ja liityin näihin puheluihin työkollegoideni kanssa yrittääkseni löytää ratkaisuja yhdessä, ja olin aina viimeinen este virhetilanteiden estämisessä useimmissa tapauksissa. Tajusin, että täytyy olla parempi, vähemmän kallista ja arvokkaampi tapa ratkaista nämä skenaariot. Niinpä syntyi idea käyttää formaaleja menetelmiä luomaan määrityksiä ennen koodin toteutusta. Aloin akateemisen matkani kohti tätä, mikä vei minut Informal Systemsiin ja Quintiin.

Quint ei alun perin ollut suunniteltu tuotteeksi. Rakensimme sen tarpeen vuoksi Informal Systemsissa. Kirjoitimme TLA+-määrityksiä järjestelmille, joita tarvitsimme luottaa enemmän kuin teimme, mutta se ei laajentunut hyvin pienen ryhmän ulkopuolelle, koska syntaksi oli liian pelottava ja työkalut eivät täyttäneet ihmisten perusodotuksia. Näytimme kollegoille ja ulkoisille yhteistyökumppaneille: “katso tätä upeaa asiaa, jonka tein”, mutta he eivät voineet lukea sitä, eivätkä heillä ollut aikaa opetella uutta työkalua.

Quintin suunnitteluratkaisut seuraavat suoraan tästä kokemuksesta. Kieli on helppo lukea ja muistaa. Ensimmäinen asia, jonka rakensimme, oli VSCode-laajennus, joka korostaa virheitä kirjoitettaessa. Sillä on tyypit ja erilliset tilat, joilla voidaan erottaa kerrokset eksplisiittisesti. Sillä on REPL, jolla voidaan tutkia interaktiivisesti, ja simulaattori, jolla voidaan saada nopea palaute ja iteroida. Se vie jäljet standardoituihin JSON-muotoon, joka on helppo koneille parseata. Nämä olivat asioita, joita ohjelmoijat odottavat työkaluistaan, ja joita tarvitsimme itse. Verifiointi alla on sama logiikka kuin TLA+:ssa.

Olen omistautunut tekemään formaalista menetelmistä helpommaksi, ja laitteiden toimittaminen on jännittävää, mutta todellinen vaikutus tulee vasta, kun insinööritoteutusryhmät todella käyttävät niitä. On edelleen ero siinä, mitä työkalut voivat tehdä, ja miten hyödyllisiä ne tuntuvat kehittäjille, ja työskentelen tämän kuilun sulkemiseksi.

Lukijoille, jotka eivät ole tuttuja siihen, miten selität, mitä Quint on ja miksi uusi määrityskieli oli tarpeen olemassa olevien työkalujen, kuten TLA+:n, rinnalla?

Useimmat määritykset ovat dokumentaatiota. Kirjoitat ylös, mitä järjestelmän pitäisi tehdä, ja tarkistat ne lukemalla. Ongelma on, että dokumentaatio on väärin tapahtumissa, joita et voi mekanisoida havaita: määrittämättömät nimet, epäselvä käyttäytyminen, oletetut oletukset. Yleensä huomaat tämän toteutuksen aikana tai tuotannossa.

Quint-määritys on jotain, mitä voit suorittaa. Mallinnat järjestelmän tilakoneena, määrität ominaisuudet, jotka sen pitäisi toteuttaa, ja suoritat tai verifioit mallin. Jos on rikkomus, saat vastaesimerkin, joka näyttää tarkalleen askelten järjestyksen, joka laukaisee sen. Tämä muuttaa, milloin ja miten halvalla havaitset suunnitteluvirheen.

TLA+ pystyi aina tekemään tämän. Quint tekee sen käytännölliseksi insinööreille, jotka eivät ole jo asiantuntijoita temporal logiikassa.

Quint on suunniteltu siltaamaan formaalisten menetelmien ja arkipäivän ohjelmistokehityksen välinen kuilu. Mitkä olivat suurimmat käytettävyyden esteet, joita pyrittiin poistamaan verrattuna perinteisiin lähestymistapoihin?

Rehellisesti sanottuna suurin käytettävyyseste oli syntaksi. Siksi aloimme syntaksista. Sen jälkeen voimme keskittyä muihin tekijöihin. Quintin tyyppi- ja vaikutusjärjestelmä tuli lippaamaan mahdollisimman monta virhettä ennen kuin aloitetaan varsinaista verifiointiprosessia, ja ihmiset arvostivat sitä paljon. Se johti siihen, että kirjoitimme laadukkaampia määrityksiä, joita vielä useammat ihmiset voivat lukea. Integroimme sen kaikki editoreihin ja tarjosimme perustoiminnallisuuden, jonka kehittäjillä on oikeus odottaa.

Suurin vaikutus sen jälkeen oli simulaattorimme. Se alkoi vain keinoena tarjota ihmisille ensimmäinen palaute järjestelmän käyttäytymisestä, koska kehittäjä haluaa pystyä jotenkin suorittamaan koodin kirjoittamisen jälkeen. Se osoittautui erittäin arvokkaaksi tapana saada luottamusta määrityksiin, jotka ovat liian suuria verifioinnin käsittelyyn, koska asiantuntijuus määritysten sovittamiseen verifioinnin mahdolliseksi tekemiseksi ei voida olettaa. Simulaattorimme teki luottamuksen helpommaksi saavuttavaksi, ja olemme käyttäneet sitä laajasti monissa projekteissa.

Suurin kipukohtani TLA+:n syntaksissa oli, kuinka usein sekoitin takakenoviivani ja normaalit viivat, ja sinun täytyy kirjoittaa niitä paljon. Pidän Quintin syntaksista paljon enemmän, mutta se, mikä tekee sen mahdottomaksi palata, on kaikki työkalut.

Yksi Quintin vahvuuksista on sen kyky mallintaa ja testata hajautettuja järjestelmiä ennen käyttöönottoa. Miten tämä muuttaa tapaa, jolla insinöörit ajattelevat järjestelmien, kuten blockchainien tai reaaliaikaisen infrastruktuurin, rakentamisesta?

Suurin muutos on siirtää validointi aikaisemmaksi. Leslie Lamport, TLA+:n luoja, vertaa määritysten kirjoittamista ennen koodia piirustusten tekemiseen ennen rakennustyötä. Vaikka olet jo rakentanut jotain ilman piirustuksia, on silti hyvä idea kirjoittaa se nyt ja käyttää sitä tulevien muutosten ohjaamiseen.

Ohjelmistoteollisuudessa käytämme markdown-tiedostoja ja valkotauluja. Ehkä voit vertailla sitä yrittämään kuvata rakennusta tekstuaalisesti. Se toimii, mutta tietäisitkö, jos seinän koot laskisivat yhteen? Quint tarjoaa tavan kuvata järjestelmiä, joissa voit olla yhtä korkealla tasolla kuin haluat, ja saada tietoa sen käyttäytymisestä ja oikeellisuudesta.

Quint perustuu TLA+:n periaatteisiin, jota käytetään laajasti hajautettujen järjestelmien kuvaamiseen. Miten tasapainosit teoreettisen tiukkuuden ylläpitämisen ja kielen kehittämisen kehittäjien kannalta ystävällisemmäksi?

Avainpäätös oli rajoittaa Quint TLA+:n fragmenttiin eikä paljastaa kaikkea, mitä logiikka sallii. TLA on erittäin ilmaisuvoimainen, ja osa tästä ilmaisuvoimaisuudesta sisältää operaattoreita, joita ei tueta työkaluilla, ja sallii yhdistelmiä, joita ihmiset ymmärtävät ja käyttävät väärin, mikä tekee siitä erittäin hankalaa debugata. Teimme tietoisen valinnan: pidä se, mitä useimmat realistiset määritykset todella tarvitsevat, ja vältä se, mikä voi aiheuttaa sekaannusta.

Tyyppijärjestelmä ja vaikutusjärjestelmä lisäävät rajoituksia, mutta rajoituksia, jotka ovat hyödyllisiä. Ne estävät koko luokan määritysvirheitä, jotka eivät ole hauskoja, kun ne havaitaan verifioinnin jo käynnistyttyä. Tyypit ovat lähes kokonaan inferoiduista ja vaikutukset ovat piilotettuina käyttäjiltä, joten se lisää arvoa ilman kitkaa.

Ennen kuin opin TLA+:n olemassaolosta, tein tutkimustyötä tyyppijärjestelmissä, mikä tarkoittaa, että Quintin tyyppitarkistin oli ehkä suosikkikomponenttini kirjoittaa. Muistan juoneeni Paçoca-makuista kahvia ensimmäisissä kuukausissa Informal Systemsissa tarkastellessani tyyppijärjestelmän paperia ja ajattellessani “elämäni on upea”.

Tehdäksi kieli hyväksi käyttää ja samalla pitää yhteyttä TLA+:n kanssa (koska Quint-määritykset voidaan transpiloida TLA+:ksi) oli ohjelmointikielen harjoitus, ja tiimin keskustelut olivat eniten avuksi, seurattuina varhaisista käyttäjien palautteista. On edelleen parannettavaa, ja se saattaa olla lempparini työssäni.

Olet myös työskennellyt staattisessa analyysissä ja tyyppijärjestelmissä. Miten nämä kokemukset ovat vaikuttaneet Quintin tyyppitarkistukseen, työkaluihin ja kehittäjien kokemukseen?

Suurin opetus, jonka opin siinä, on, etteivät kaikki kielet ole samanlaisia. Kuulet ihmisiä sanovan, että se on vain uuden syntaksin oppimista, ja kaikki samat käsitteet ovat edelleen sovellettavissa, joten kaikki kielet ovat samanarvoisia, ja se on vain makua. Tämä ei ole totta. Ohjelmointikielen tutkimus on suuri ala, jossa tutkijat tekevät upeaa työtä edistääkseen tätä alaa, eikä se ole vain siinä, että kieli näyttää paremmalta tai miellyttävämmältä.

Funktionaalinen ohjelmointi esiteltiin minulle varhain, ja opin Haskellin yhtä aikaa kuin C:n (ensimmäinen ohjelmointikieleni), ja olen siitä kiitollinen. Tämä on perusta, joka auttaa minua näkemään, että erottelu tilamuutoksista ja epädeterminismistä ohuksi kerrokseen Quintissä ja kaiken monimutkaisuuden sijoittaminen puhdistiin funktioihin auttaa objektiivisesti monilla tekijöillä, eikä se ole vain makua. En usko, että Quintin rakentaminen olisi ollut tuottavaa, jos makua olisi usein keskustelun aiheena.

Opettamalla formaaleja menetelmiä luennoitsijana sinulla on ainutlaatuinen näkökulma. Mitkä ovat yleisimmät väärinkäsitykset, joita insinöörit ovat formaalisen verifioinnista tänään?

No, opetin alokkaita, jotka olivat vasta aloittamassa uraansa teollisuudessa. Suurin osa heistä ei ollut kuullut formaalisten menetelmien tai formaalisen verifioinnin kaltaisista aiheista. Opetin heille, miten formaalisten menetelmien ja formaalisen määrityksen avulla voidaan parantaa ratkaisujen ja reunatapausten löytämistä. Toivon, että kun he kohtaavat vastaavan tilanteen työssään, he muistavat minun.

On kasvava kiinnostus yhdistää tekoäly ohjelmistokehitykseen. Näetkö roolin tekoälyllä auttamassa kehittäjiä kirjoittamaan, validoimaan tai jopa generoimaan formaaleja määrityksiä työkaluilla, kuten Quint?

Merkitsevä, ja se on jo tapahtumassa. Tietojenkäsittelytiede on laajempi kuin koodin kirjoittaminen, ja tekoäly avaa oven täysin uusiin tavoisiin käyttää formaaleja menetelmiä. LLM:t ovat hyviä kirjoittamaan Quint-määrityksiä luonnollisen kielen kuvausten perusteella järjestelmistä ja jopa olemassa olevasta koodista. Quint LLM -paketti sisältää Claude Code -agenteja, jotka ottavat englanninkielisen kuvausprotokollan ja tuottavat Quint-määrityksen, jonka voit suorittaa ja tarkistaa välittömästi.

Samalla Quint auttaa kehittäjiä luottamaan koodiin, jota on kirjoitettu tekoälyllä. Uskon vahvasti, että luottamus tulee ymmärryksestä, ei jostakin maagisesta tarkistusmerkistä. Työskentelemällä Quint-määrityksellä, joka ohjaa ja tarkistaa toteutuskoodeja, kehittäjät voivat edelleen omistaa ja ymmärtää järjestelmän käyttäytymistä, ja ratkaista kognitiivisen velan ongelman, jonka tekoälyn käyttäminen voi luoda, ja tarjota vakuuttavamman tavan validoida generoitu koodi.

Hyödynnämme LLM:itä kieli-työkaluina, jotka kirjoittavat Quintin tarkat määritykset luonnollisen kielen intentistä, ja sitten annamme Quint-työkalut tekoälylle, jotta se voi suorittaa asioita, joita se ei voi luotettavasti tehdä itse, kuten löytää reunatapauksia.

Mitä täytyy tapahtua, jotta formaalisten menetelmien käyttö siirtyy niukasta omaksumisesta standardiosaksi osaksi ohjelmistokehityksen elinkaarta?

Jo jonkin aikaa tiedän, että kaksi tärkeintä asiaa, joita Quint tarvitsee enemmän omaksumista varten, ovat alhaisempi kustannus ja suurempi arvo. Uskon, että tämä koskee monia muita asioita. Formaalisten menetelmien sai suuren lisäyksen molemmissa näissä tekijöissä, kun tekoäly vähentää formaalisten määritysten kirjoittamisen kustannuksia ja luo ympäristön, jossa formaalisten menetelmien puute luottamusta ja ymmärrystä, jossa formaalisten menetelmien vaikutus on suurin ja arvokkain, ja toivon, että tämä muutos on suuntautunut korkeamman tason suunnittelupäätöksiin ja käyttäytymisen oikeellisuuteen, mikä tekee formaalisten menetelmistä jokapäiväisen työkalun, eikä siitä, että emme ymmärrä koodia tai järjestelmiä enää, ja vietämme koko aikamme tarkastamalla tekoälyllä generoituja koodauksia ilman työkaluja, joiden avulla voimme ymmärtää niitä.

Kiitos tästä haastattelusta; lukijoille, jotka ovat kiinnostuneita oppimaan lisää tästä suoritettavasta määrityskielen kieli mallintamiseen ja verifioimiseen monimutkaisia järjestelmiä, mukaan lukien sen työkalut ja miten aloittaa, voivat tutkia Quintiä.