Gabriela Moreira, CEO of Quint at Informal Systems – Interview Series

Gabriela Moreira, CEO of Quint at Informal Systems, jest inżynierem badawczym specjalizującym się w językach programowania i metodach formalnych, z silnym naciskiem na tworzenie narzędzi, które sprawiają, że weryfikacja złożonych systemów jest bardziej dostępna dla inżynierów. Kieruje rozwojem Quint, nowoczesnego języka specyfikacji wykonywalnych opartego na TLA+, gdzie kontynuuje prace nad rozwojem języka i jego narzędzi. Jej praca obejmuje weryfikację formalną, analizę statyczną i narzędzia dla programistów, a także wniosła wkład w dziedzinę akademicką, ucząc metod formalnych, co odzwierciedla połączenie praktycznej inżynierii i głębi teoretycznej.

Quint, opracowany i utrzymywany przez Informal Systems, to nowoczesny język specyfikacji zaprojektowany do modelowania, testowania i weryfikacji złożonych systemów, takich jak sieci rozproszone, blockchain i bazy danych. Zbudowany na podstawie Temporal Logic of Actions (TLA), Quint wprowadza bardziej przyjazny dla programistów składnię, wraz z zaawansowanym narzędziem, takim jak sprawdzanie typów, symulacja i weryfikacja modelu, co pozwala inżynierom wykrywać awarie systemu przed wdrożeniem. Platforma kładzie nacisk na wykonywalne specyfikacje, umożliwiając programistom nie tylko opisywać zachowanie systemu, ale także aktywnie testować i eksplorować je, zamykając lukę między teoretyczną poprawnością a realizacją w świecie rzeczywistym.

Cofnijmy się do początku, co pierwsze zainteresowało Cię programowaniem, i jak ostatecznie trafiłaś na metody formalne i systemy rozproszone?

Byłam zapalona graczką z złym komputerem i zorientowałam się, że lubię naprawiać problemy i sprawiać, by działał. Zapisalam się na informatykę i zainteresowałam się teorią i kompilatorami.

W 2015 roku zostałam przedstawiona konkursom programistycznym. W tych konkursach zazwyczaj otrzymujesz kilka przykładów wejścia i oczekiwanego wyjścia, a następnie piszesz kod, który rozwiązuje problem i działa dla tych przykładów. Jednak po przesłaniu go do oceny kod jest naprawdę testowany z wieloma więcej przykładami poza tymi, które są pokazane. To zrozumienie, że kod może działać dla scenariuszy, które widzę lub o których myślę, ale nadal może awariować w przypadkach, których nie rozważałam, uczyniło programowanie rodzajem wyzwania, w które się zakochałam.

Pracując w branży, szybko zainteresowałam się systemami rozproszonymi, w których musieliśmy brać pod uwagę różne kolejności, w jakich mogą przychodzić wiadomości, różne tryby awarii i cały świat ukrytych zachowań. W 2018 roku kolega przedstawił mi język specyfikacji formalnej o nazwie TLA+. Byłam zaangażowana. Natychmiast zaczęłam budować narzędzia wokół TLA+ i od tego czasu pracuję w tym obszarze.

Zbudowałaś swoją karierę wokół metod formalnych i języków programowania, od wczesnej pracy nad narzędziami opartymi na Temporal Logic of Actions (TLA+) do kierowania rozwojem Quint w Informal Systems. Co motywowało Cię do skoncentrowania się na tym, aby weryfikacja formalna była bardziej dostępna, i jak ta wizja ukształtowała projekt Quint?

TLA+ jest zbyt dobre, aby nie być używane szeroko w branży. Byłam jeszcze dość młoda, kiedy dowiedziałam się o tym, i dołączałam do tych połączeń z moimi kolegami z pracy, aby próbować wspólnie znaleźć rozwiązania, i zawsze znajdowałam scenariusze, w których nasze rozwiązania zawiodły. Jednak zawsze byłam ostatnią linią obrony przed tymi scenariuszami w większości przypadków. Zorientowałam się, że musi być lepszy, mniej kosztowny i bardziej wartościowy sposób rozwiązywania tych scenariuszy. W ten sposób powstał pomysł użycia metod formalnych do tworzenia specyfikacji przed implementacją kodu. Więc zaczęłam swoją podróż akademicką w tym kierunku, co doprowadziło mnie do Informal Systems i Quint.

Quint nie został początkowo wymyślony jako produkt. Zbudowaliśmy go z necessity w Informal Systems. Pisaliśmy specyfikacje TLA+ dla systemów, którym musieliśmy bardziej ufać, niż robiliśmy, ale to nie rozprzestrzeniło się poza bardzo małą grupę ludzi, ponieważ składnia była zbyt straszna z zbyt wieloma symbolami matematycznymi, a narzędzia nie spełniały podstawowych oczekiwań ludzi. Pokazywaliśmy kolegom i zewnętrznym współpracownikom: „spójrzcie na tę wspaniałą rzecz, którą zrobiłam”, ale oni nie mogli jej przeczytać i nie mieli czasu, aby nauczyć się nowego narzędzia.

Wybory projektowe w Quint wynikają bezpośrednio z tego doświadczenia. Język jest łatwy do czytania i zapamiętania. Pierwszą rzeczą, którą zbudowaliśmy, była rozszerzenie VSCode, które podświetla błędy podczas pisania. Ma typy i różne tryby, aby oddzielić warstwy wyraźnie. Ma REPL, aby można było eksplorować interaktywnie, i symulator, aby można było uzyskać szybką informację zwrotną i iterować. Eksportuje ślady do standardowego formatu JSON, który jest łatwy do przetworzenia przez maszyny. Były to rzeczy, których oczekiwali już programiści i których potrzebowaliśmy sami. Weryfikacja pod spodem jest tą samą logiką co TLA+.

Jestem obsesyjnie zaangażowana w to, aby metody formalne były bardziej dostępne, a wysyłanie narzędzi jest ekscytujące, ale prawdziwy wpływ jest odczuwalny tylko wtedy, gdy zespoły inżynierskie naprawdę ich używają. Jest jeszcze różnica między tym, co narzędzia mogą zrobić, a tym, jak użyteczne wydają się programistom, i pracuję nad tym, aby tę lukę zamknąć.

Dla czytelników, którzy nie są zaznajomieni z tym, jak wyjaśnisz, co to jest Quint i dlaczego potrzebny jest nowy język specyfikacji obok istniejących narzędzi, takich jak TLA+?

Większość specyfikacji to dokumentacja. Piszesz, co system powinien robić, i sprawdzasz je przez czytanie. Problem polega na tym, że dokumentacja jest błędna w sposób, który nie może być mechanicznie wykryty: niezdefiniowane nazwy, niejednoznaczne zachowanie, niejawne założenia. Zazwyczaj dowiadujesz się o tym podczas implementacji lub w produkcji.

Specyfikacja Quint to coś, co można wykonać. Modelujesz system jako maszynę stanu, definiujesz właściwości, które powinien spełniać, i uruchamiasz lub weryfikujesz model. Jeśli istnieje naruszenie, otrzymujesz przykład pokazujący dokładną sekwencję kroków, które wyzwala to naruszenie. To zmienia, kiedy i jak tanio złapiesz błąd projektowy.

TLA+ mógł to zrobić od zawsze. Quint sprawia, że jest to praktyczne dla inżynierów, którzy nie są już specjalistami w logice temporalnej.

Quint jest zaprojektowany, aby zabić lukę między metodami formalnymi a codziennym inżynierią oprogramowania. Jakie były największe bariery użyteczności, które chciałaś wyeliminować w porównaniu z tradycyjnymi podejściami?

Szczerze, największą barierą użyteczności była składnia. Dlatego zaczęliśmy od składni. Po rozwiązaniu tego problemu mogliśmy się bardziej skoncentrować na innych czynnikach. System typów i efektów w Quint służy do oznaczenia tak wielu błędów, jak to tylko możliwe, zanim jeszcze rozpocznie się zwykły proces weryfikacji, i ludzie bardzo cenili sobie to. To doprowadziło do napisania lepszych specyfikacji, które mogli przeczytać jeszcze więcej ludzi. Zintegrowaliśmy to wszystko w edytorach i zapewniliśmy podstawową funkcjonalność, której oczekują wszyscy programiści.

Największy wpływ po tym był nasz symulator. Zaczęło się jako sposób, aby dać ludziom pierwszą informację zwrotną o zachowaniu ich systemu, jako że programista chce móc w jakiś sposób uruchomić kod po jego napisaniu. Okazało się, że jest to niezwykle wartościowe jako sposób, aby uzyskać pewność co do specyfikacji, które są zbyt duże, aby weryfikacja mogła się nimi zajmować, ponieważ umiejętność adaptacji specyfikacji do celów weryfikacji nie powinna być przyjmowana za pewnik. Nasz symulator sprawił, że ta pewność stała się bardziej dostępna, i używaliśmy go intensywnie w wielu projektach.

Mój największy ból głowy związany z składnią TLA+ polegał na tym, jak często myliłam backslashy i regularne slashy, i trzeba je wpisywać wiele razy. Lubię składnię Quint bardziej, ale to, co naprawdę sprawia, że nie mogę wrócić do TLA+, to wszystkie narzędzia.

Jedną z największych sił Quint jest jego zdolność do modelowania i testowania systemów rozproszonych przed wdrożeniem. Jak to zmienia sposób, w jaki inżynierowie powinni myśleć o budowaniu systemów, takich jak blockchain lub infrastruktura w czasie rzeczywistym?

Największa zmiana polega na przeniesieniu walidacji na wcześniejszy etap. Leslie Lamport, twórca TLA+, porównuje pisanie specyfikacji przed kodem do tworzenia planów budowlanych przed rozpoczęciem robót budowlanych. Nawet jeśli już coś zbudowaliśmy bez planu, nadal jest to dobry pomysł, aby napisać go teraz i użyć do poinformowania dalszych zmian.

W branży oprogramowania używamy plików markdown i tablic. Można to porównać do próby opisania budynku za pomocą tekstu. Działa to, ale czy wiesz, czy rozmiary ścian się zgadzają? Quint oferuje sposób opisu systemów, w którym możesz być tak abstrakcyjny, jak chcesz, i uzyskać wgląd w jego zachowanie i poprawność.

Quint opiera się na podstawach TLA+, który jest powszechnie używany do opisu systemów rozproszonych. Jak zbalansowałaś utrzymanie tej teoretycznej surowości przy jednoczesnym uczynieniu języka bardziej przyjaznym dla programistów?

Kluczową decyzją było ograniczenie Quint do fragmentu TLA (logiki za TLA+) zamiast eksponowania wszystkiego, co pozwala na to logika. TLA jest bardzo wyrafinowane, a część tej wyrafinowania obejmuje operatory, które nie są obsługiwane przez żadne narzędzia, i pozwala na połączenia, których ludzie rozumieją i używają w sposób mylący, co sprawia, że jest to bardzo trudne do debugowania. Zrobiliśmy świadomą decyzję: trzymajmy się tego, co najbardziej realistyczne specyfikacje naprawdę potrzebują, i unikajmy tego, co ma potencjał do zamieszania.

System typów i efektów dodaje ograniczenia, ale ograniczenia, które są użyteczne. Zapobiegają one całej klasie błędów specyfikacji, które nie są przyjemne, gdy zostaną znalezione po uruchomieniu weryfikacji. Typy są niemal całkowicie wnioskowane, a efekty są ukryte przed użytkownikami, więc to dodaje wartość bez tarcia.

Zanim dowiedziałam się o istnieniu TLA+, robiłam prace badawcze nad systemami typów, co oznacza, że sprawdzanie typów w Quint było prawdopodobnie moim ulubionym komponentem do napisania. Pamiętam, że piłam kawę o smaku Paçoca w moich pierwszych miesiącach w Informal, przeglądając jakiś artykuł o systemie typów i myśląc: „moje życie jest niesamowite”.

Uczynienie języka dobrym w użyciu, a jednocześnie zachowanie korespondencji z TLA+ (ponieważ specyfikacje Quint mogą być transliterowane do TLA+) było ćwiczeniem z języka programowania, a dyskusje z zespołem były najbardziej pomocnym zasobem, po którym następowała opinia wczesnych użytkowników. Jest jeszcze kilka ulepszeń, które chcemy wprowadzić, i to może być moja ulubiona część pracy.

Także pracowałaś nad analizą statyczną i systemami typów. Jak doświadczenia te wpłynęły na sprawdzanie typów w Quint, narzędzia i ogólne doświadczenie programisty?

Największa lekcja, jaką nauczyłam się w tym świecie, jest taka, że nie wszystkie języki są takie same. Słyszałam, jak ludzie mówią, że to tylko kwestia nauki nowej składni, te same pojęcia nadal mają zastosowanie, więc wszystkie języki są równe i to tylko kwestia gustu. To nie jest prawda. Dziedzina języków programowania ma wielkich badaczy, którzy robią niesamowitą pracę, aby ten obszar posuwać do przodu, i to nie tylko po to, aby uczynić język wyglądającym ładniej lub bardziej po ich myśli.

Programowanie funkcyjne zostało mi przedstawione bardzo wcześnie, nauczyłam się Haskell w tym samym czasie, co C (mój pierwszy język programowania), i jestem bardzo wdzięczna za to. To jest podstawa, która pomaga mi zobaczyć, że izolowanie mutacji stanu i nieprzewidywalności do cienkiej warstwy w Quint, i mając wszystką złożoność w czystych funkcjach, obiektywnie pomaga w wielu czynnikach, i to nie jest tylko kwestia gustu. Nie myślę, że budowanie Quint byłoby produktywne, gdyby kwestie gustu były zbyt często dyskutowane.

Nauczanie metod formalnych jako wykładowca daje Ci unikalną perspektywę. Jakie są najczęstsze nieporozumienia, jakie inżynierowie mają na temat weryfikacji formalnej dzisiaj?

Cóż, uczyłam studentów pierwszego stopnia, którzy dopiero wkraczali w branżę. Ogromna większość z nich nigdy wcześniej nie słyszała o metodach formalnych ani weryfikacji formalnej, więc nie było żadnych nieporozumień! Program nauczania został tak opracowany, aby większość z nich nie uczyła się o systemach rozproszonych, a około połowa z nich uczyła się o wątkach w tym samym semestrze. Mówiłam im, że czuję się, jakbym uczyła ich, czym jest parasol, zanim doświadczyli deszczu!

Byłam bardziej zmotywowana do nauczenia ich, jak metody formalne i formalne specyfikowanie systemu mogą pomóc w rozwiązywaniu problemów i znajdowaniu przypadków brzegowych, niż do tego, aby myśleli, że powinni formalnie weryfikować każde oprogramowanie, które kiedykolwiek napiszą. Mój ostatni projekt był ustawiony jako gra RPG, w której różne kolejności, w jakich mogli grać, i różne ustawienia musiały być brane pod uwagę, starając się naśladować trudności, z którymi mamy do czynienia w systemach rozproszonych, jak najwięcej. To się powiodło, bo było wystarczająco trudne, aby musieli użyć narzędzi, aby znaleźć przypadki brzegowe i poprawić swoje rozwiązania, aby pokonać potwory na końcu. Mam nadzieję, że kiedy kiedyś spotkają podobną sytuację w pracy, będą pamiętać o mnie. Niektórzy z nich już to zrobili.

Istnieje rosnące zainteresowanie łączeniem AI z rozwojem oprogramowania. Czy widzisz rolę dla AI w pomocy programistom w pisaniu, walidowaniu lub nawet generowaniu formalnych specyfikacji przy użyciu narzędzi takich jak Quint?

Istotną, i już się to dzieje. Informatyka jest większa niż pisanie kodu, a AI otwiera drzwi do całkowicie nowych sposobów korzystania z metod formalnych. LLM są dobre w pisaniu specyfikacji Quint z opisów języka naturalnego systemu i nawet istniejącego kodu. Kit LLM Quint ma agenci Claude Code, którzy biorą opis angielski protokołu i produkują specyfikację Quint, którą można uruchomić i sprawdzić natychmiast.

W tym samym czasie Quint również pomaga programistom ufać kodowi napisanemu z AI. Uważam, że zaufanie musi pochodzić z zrozumienia, a nie jakichś magicznych znaczników. Pracowanie nad specyfikacją Quint, która naprowadza i sprawdza kod implementacyjny, oznacza, że programiści mogą nadal władać i rozumieć zachowania systemu, rozwiązując dług techniczny, jaki może powstać w wyniku użycia AI, i dostarczając bardziej pewne sposoby weryfikacji wygenerowanego kodu.

Wykorzystujemy LLM jako narzędzia językowe, które piszą dokładne definicje Quint z naturalnego języka intencji, a następnie dajemy narzędzia Quint AI, aby mogła osiągnąć rzeczy, których nie może sama zrobić, takie jak znajdowanie przypadków brzegowych.

Spójrzając w przyszłość, co musi się wydarzyć, aby metody formalne przeszły od niszy do standardowej części cyklu rozwoju oprogramowania?

Od jakiegoś czasu wiem, że dwie rzeczy, których Quint potrzebuje do większej akceptacji, to niższy koszt i wyższa wartość. Myślę, że to dotyczy również wielu innych rzeczy. Metody formalne właśnie otrzymały duży zastrzyk w obie te rzeczy, z AI znacznie zmniejszającym koszt pisania formalnych specyfikacji i tworzącym środowisko braku zaufania i zrozumienia, w którym metody formalne mogą mieć największy wpływ i wartość.

Zmieniając się z AI, która zmienia nasz zawód, przynajmniej do pewnego stopnia, mam nadzieję, że ta zmiana jest w kierunku wyższych decyzji projektowych i poprawności zachowania, czyniąc metody formalne codziennym narzędziem; i nie w kierunku niezrozumienia przez nas kodu ani systemów i spędzania całego czasu na przeglądaniu kodu wygenerowanego przez AI bez żadnych narzędzi, które mogą nam pomóc w zrozumieniu.

Dziękuję za wnikliwy wywiad; czytelnicy zainteresowani dowiedzeniem się więcej o tym języku specyfikacji wykonywalnych do modelowania i weryfikacji złożonych systemów, w tym jego narzędziach i jak zacząć, mogą odwiedzić Quint.