Gabriela Moreira, CEO Quint w Informal Systems – Wywiad

Gabriela Moreira, CEO Quint w 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 nadal utrzymuje i rozwija język oraz jego narzędzia. Jej praca obejmuje weryfikację formalną, analizę statyczną i narzędzia programistyczne, a także przyczyniła się do rozwoju akademickiego, nauczając metod formalnych, co odzwierciedla połączenie praktycznej inżynierii i głębi teoretycznej.

Quint, rozwijany i utrzymywany w 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 sprawdzanie 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 rzeczywistą implementacją.

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

Byłam zapalona graczką z złym komputerem i zrozumiałam, że lubię naprawiać problemy i sprawiać, by działał. Zapiszę się na informatykę i byłem przyciągany do teorii i kompilatorów. 

W 2015 roku zostałam zaproszona do konkursów programistycznych. W nich 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 rzeczywiście 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 zostałam przyciągnięta do systemów rozproszonych, gdzie 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 zauroczona. Natychmiast zaczęłam budować narzędzia wokół TLA+ i od tego czasu pracuję w tym obszarze.

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

TLA+ jest zbyt dobry, aby nie być używany 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ć znaleźć rozwiązania razem, i zawsze znajdowałam scenariusze, w których nasze rozwiązania byłyby niewłaściwe. Jednak zawsze była ostatnią linią obrony przed tymi scenariuszami w większości przypadków. Zdecydowałam, że musi być lepszy, mniej kosztowny i bardziej wartościowy sposób rozwiązywania tych scenariuszy. Tak 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 zaprojektowany 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 to wspaniałe, co zrobiłam”, ale oni nie mogli go 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 wyraźne tryby, aby wyraźnie oddzielić warstwy. 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 programiści od swoich narzędzi i których potrzebowaliśmy sami. Weryfikacja pod spodem jest tą samą logiką co TLA+.

Jestem obsesyjnie zainteresowana uczynieniem metod formalnych bardziej dostępnymi, a wysyłanie narzędzi jest ekscytujące, ale prawdziwy wpływ jest odczuwalny tylko wtedy, gdy zespoły inżynierskie naprawdę je używają. Jest jeszcze delta między tym, co narzędzia mogą zrobić, a tym, jak użyteczne wydają się programistom, i pracuję nad zamknięciem tej luki.

Dla czytelników, którzy nie są zaznajomieni z tym, jak byś wyjaśniła, 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 zachowania, niejawne założenia. Zazwyczaj dowiadujesz się o tym podczas implementacji lub w produkcji.

Specyfikacja Quint to coś, co wykonuje się. 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ładnie sekwencję kroków, które wyzwala je. To zmienia, kiedy i jak tanio złapiesz błąd projektu.

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

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

Szczerze mówiąc, 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 Quint flaguje tyle błędów specyfikacji, ile to możliwe, zanim jeszcze rozpocznie się regularny proces weryfikacji, i ludzie bardzo cenili sobie to. To doprowadziło do napisania lepszych specyfikacji, które jeszcze więcej ludzi mogło przeczytać. Zintegrowaliśmy to wszystko w edytorach i oferowaliśmy podstawową funkcjonalność, której oczekują wszyscy programiści.

Największy wpływ po tym miał nasz symulator. Zaczęło się jako sposób, aby dać ludziom pierwszą informację zwrotną o zachowaniu ich systemu, jak programiści chcieliby, aby móc jakoś uruchomić kod po napisaniu. Okazało się, że jest to niezwykle wartościowe jako sposób, aby uzyskać zaufanie do specyfikacji, które są zbyt duże, aby weryfikacja mogła je obsłużyć, ponieważ ekspertyza adaptacji specyfikacji do uczynienia jej wykonalną dla weryfikacji nie powinna być przyjmowana za pewnik. Nasz symulator uczynił zaufanie bardziej dostępnym 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 mieszane były moje backslashy i regularne slashy, i trzeba je dużo pisać. 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 zalet 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 prac budowlanych. Nawet jeśli już coś zbudowaliśmy bez planu, nadal jest to dobra idea, aby go napisać teraz i użyć go 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 wymiary ścian się zgadzają? Quint oferuje sposób opisu systemów, w którym możesz być tak abstrakcyjny, jak chcesz, i uzyskać informacje o jego zachowaniu i poprawności.

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, uczynienie języka bardziej przyjaznym dla programistów?

Kluczowa decyzja polegała na ograniczeniu Quint do fragmentu TLA (logiki za TLA+) zamiast eksponowania wszystkiego, co logika pozwala. TLA jest bardzo wyrafinowany, a część tej wyrafinowania obejmuje operatory, które nie są obsługiwane przez żadne narzędzia, i pozwala na połączenia, które ludzie rozumieją i używają w sposób niepoprawny, co sprawia, że jest to bardzo trudne do debugowania. Zrobiliśmy świadomą decyzję: trzymajmy się tego, co większość realistycznych specyfikacji naprawdę potrzebuje, i unikajmy tego, co ma potencjał ku pomyłkom.

System typów i efektów dodaje ograniczenia, ale są to ograniczenia, które są użyteczne. Zapobiegają one całej klasie błędów specyfikacji, które nie są zabawne, gdy zostaną znalezione po rozpoczęciu weryfikacji. Typy są prawie w całości inferowane, 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 Quint było prawdopodobnie moim ulubionym komponentem do napisania. Pamiętam, jak 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ślałam: „moje życie jest niesamowite”. 

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

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

Największa lekcja, jaką nauczyłam się w tym świecie, polega na tym, że nie wszystkie języki są takie same. Słyszysz, jak ludzie mówią, że jest to tylko kwestia nauczenia się nowej składni, te same pojęcia nadal mają zastosowanie, więc wszystkie języki są równe i jest to tylko kwestia gustu. To nie jest prawda. Dziedzina języków programowania ma wspaniałych badaczy, którzy robią niesamowitą pracę, aby posunąć tę dziedzinę do przodu, i to nie jest tylko kwestia uczynienia języka bardziej atrakcyjnym lub bardziej odpowiednim do ich gustu.

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 za to bardzo wdzięczna. To jest podstawa, która pomaga mi zobaczyć, że izolowanie mutacji stanu i nieoznaczoności do cienkiej warstwy w Quint, i posiadanie wszystkiej złożoności w czystych funkcjach, obiektywnie pomaga we wielu czynnikach, i to nie jest tylko kwestia gustu. Nie sądzę, aby budowanie Quint było produktywne, gdyby sprawy gustu były często dyskutowane.

Nauczanie metod formalnych jako wykładowca daje Ci unikalną perspektywę. Jakie są najczęstsze złudzenia inżynierów na temat weryfikacji formalnej dzisiaj?

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

Byłam bardziej zmotywowana do nauczenia ich, jak metody formalne i formalne specyfikowanie systemu mogą pomóc nam rozumieć rozwiązania i znajdować przypadki brzegowe, niż do zmuszania ich do myślenia, ż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 gracze mogli podejmować działania, i różne ustawienia musiały być brane pod uwagę, próbując naśladować trudności, z którymi mamy do czynienia w systemach rozproszonych, jak najbardziej. 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 będą mieć do czynienia z 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ę 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.

Jednocześnie Quint również pomaga programistom ufać kodowi napisanemu z AI. Uważam, że zaufanie musi pochodzić z zrozumienia, a nie jakiegoś magicznego sprawdzenia. Pracowanie nad specyfikacją Quint, która napędza i sprawdza kod implementacyjny, oznacza, że programiści mogą nadal władać i rozumieć zachowania systemu, rozwiązując dług kognitywny, jaki może powstać w wyniku użycia AI, i zapewniając bardziej pewne sposoby walidacji wygenerowanego kodu.

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

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

Od jakiegoś czasu wiem, że dwie rzeczy, które Quint potrzebuje, aby zwiększyć przyjęcie, to niższy koszt i wyższa wartość. Uważam, że to dotyczy wielu innych rzeczy. Metody formalne właśnie otrzymały duży zastrzyk w obu tych obszarach, z AI znacznie redukują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ść.

Z AI zmieniającym to, czym jest nasz zawód, przynajmniej do pewnego stopnia, mam nadzieję, że ta zmiana będzie ku projektowaniu na wyższym poziomie i poprawności zachowania, czyniąc metody formalne codziennym narzędziem; a nie ku temu, że nie będziemy rozumieć żadnego kodu ani systemów, i będziemy spędzać cały czas na przeglądaniu kodu wygenerowanego przez AI bez żadnego narzędzia, które mogłoby nam pomóc w zrozumieniu go.

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ędzi i sposobu rozpoczęcia, mogą zapoznać się z Quint.