Logiki temporalne, programowanie funkcyjne i perkusja. O swoich pasjach, pracach i projektach opowiada nam Marek Adamek – Custom Software Developer w Finture, a po godzinach perkusista punkrockowej grupy Pull the Wire.

Zacznijmy od gratulacji – bo widziałam, że wygraliście…?

Dziękuję! Tak, wygraliśmy plebiscyt na Złotego Bączka [1]. W zeszłym roku mieliśmy przyjemność zagrać na Małej Scenie festiwalu Pol’and’Rock. Nasz występ został doceniony przez publiczność i w tym roku – jako laureaci – zagramy na Dużej Scenie.

Grasz na perkusji. Od dawna?

Pierwszy raz z perkusją miałem styczność w wieku bodajże 13 lat, to były początki gimnazjum. Tak naprawdę chciałem grać na gitarze, ale w mojej miejscowości był tylko jeden nauczyciel gry na tym instrumencie i wiecznie był zajęty. Pamiętam, że czekałem w Gminnym Ośrodku Kultury, aż skończy zajęcia z inną osobą. Na scenie akurat stała perkusja. Spróbowałem – i tak już zostało. Lekcji gry na gitarze ani wtedy, ani później już nie odbyłem.

Prosta arytmetyka wskazywałaby, że gram już… 22 lata, ale to nie do końca prawda. Miałem dość długie przerwy, z różnych powodów: raz był to Erasmus, raz roczny wyjazd służbowy do Korei, innym razem uczelnia i doktorat, lub też inne sprawy, które wybijały mnie z – nomen omen – rytmu.

Dużo czasu musisz poświęcać na granie i ćwiczenie?

Kiedyś trenowałem więcej. Teraz – ze względów zawodowych, ale też zespołowych – mam na to mniej czasu. Bywają okresy, kiedy ćwiczenia ograniczają się do przygotowań do koncertów, a granie – do zagrania tych koncertów. Szlifowanie techniki schodzi na dalszy plan, nad czym ubolewam.

Wspomniałeś coś o służbowym wyjeździe do Korei…

Tak, byłem wtedy zatrudniony w Samsungu, gdzie wziąłem udział programie Global Mobility. Były to półroczne, roczne lub dwuletnie wymiany pracownicze pomiędzy centralą w Korei a oddziałami w innych krajach, coś na podobieństwo Erasmusa.

Wspominam ten wyjazd bardzo dobrze. Najciekawsze było poznawanie kraju i jego kultury, w tym kultury pracy, mocno odmiennej od tej, którą znałem z Polski. Było to o tyle interesujące, że przed wyjazdem i w jego trakcie byłem zaangażowany w ten sam projekt. Zakres moich obowiązków nie zmienił się znacznie, za to zmienił się sposób ich wykonywania, począwszy od precyzowania wymagań po prezentowanie i dokumentowanie wyników.

Ciekawe były też emocje, które towarzyszyły mi na różnych etapach pobytu – od fascynacji na początku, przez zdziwienie, niezrozumienie, chwilami frustrację, po – koniec końców – akceptację.

Zostałeś fanem K-popu?

(Śmiech) Owszem, ekspozycja na K-pop była duża i przewlekła. Fanem chyba nie zostałem, ale też nie gardzę. Były piosenki, które mi się podobały i które od czasu do czasu grają mi w głowie.

Karaoke było?

Było! W Noraebangach [2]. Polecam!

To był ten moment, kiedy postanowiłeś zrobić doktorat czy doktorat był wcześniej?

Doktorat zaczął się wcześniej i był w trakcie, choć zamrożony. Studia doktoranckie zacząłem krótko po zakończeniu magisterskich. Wyjazd do Korei tymczasowo zawiesił zarówno perkusję jak i doktorat. Był jedną z przyczyn, przez które moje studia doktoranckie trwały przeraźliwie długo, bo 6 lat.

Można dłużej.

Nie przeczę, jednak w moim przypadku – jeśli chciałem mieć i tytuł, i ukończone studia doktoranckie – 6 lat to było maksimum. I tyle też to trwało, bo nad doktoratem pracowałem w zasadzie po godzinach i po koncertach.

Właściwie, w takim razie, dlaczego doktorat? Z chęci zgłębienia jakiegoś kawałka wiedzy czy z jakiegoś innego powodu?

W tamtym czasie rozważałem karierę akademicką, w pewnym stopniu nadal biorę taki scenariusz pod uwagę. Czy bardziej byłaby to praca naukowa, czy dydaktyczna – nie wiem, preferencje zmieniają się w czasie.

Promotorem moich wcześniejszych prac dyplomowych był profesor Jan Mulawka i to on zaproponował mi doktorat u siebie w Zakładzie Sztucznej Inteligencji na Wydziale Elektroniki i Technik Informacyjnych. Jako że rozważałem doktorat już wcześniej, to długo się nie zastanawiałem. Tym bardziej, że pracę inżynierską i magisterską pisało mi się pod jego okiem sprawnie, szybko i przyjemnie. Z doktoratem będzie podobnie – myślałem. Jak się później okazało, pomyliłem się (śmiech).

Temat twojej pracy to „Rozwój aplikacji logik temporalnych w zastosowaniach informatycznych”. Przyznaję, dla mnie, laika – jestem tylko po roku studiów informatycznych – to dość trudne. A próbowałam czytać! Mógłbyś przybliżyć, czego dotyczy Twoja praca?

Logiki temporalne to, w skrócie, rozszerzenie logiki klasycznej. W takich logikach wyróżnia się dodatkowe operatory, które umożliwiają definiowanie formuł logicznych uwzględniających czas oraz wnioskowanie z ich wykorzystaniem. Takie operatory to np. „następnie”, „zawsze” „kiedyś”, „dopóki”. Za ich pomocą można opisać zmiany wartości zdań logicznych w czasie. Logiki temporalne mają więc – w porównaniu do logiki klasycznej – większą siłę ekspresji. W takiej logice można wyrazić więcej.

Temporalnych systemów logicznych jest wiele. W swojej pracy badałem logikę LNC (Logic Next Change), będącą specyficznym fragmentem logiki LTL opartej na dyskretnej i liniowej strukturze czasu.

LNC to pełny system logiczny, zaproponowany przez dr hab. Kordulę Świętorzecką. Na początku moje badania dotyczyły możliwości implementacji maszynowej rachunku LNC, czyli systemu, który umożliwiałby wnioskowanie w tej logice. Jednak im dłużej przyglądałem się logice LNC, tym bardziej przypominała mi logikę LTL, o której w nauce powiedziano i napisano już chyba wszystko. I miałem rację. Logika LNC okazała się być podzbiorem rachunku LTL, ale takim, który ma bardzo ciekawe właściwości.

Zasadnicza część mojego doktoratu dotyczyła wykazania, że dwa główne problemy, jakie rozważa się w przypadku logik temporalnych – czyli problem spełnialności oraz problem weryfikacji modelowej – są w przypadku LNC problemami NP-zupełnymi [3], podczas gdy dla pełnego rachunku LTL są to problemy PSPACE-zupełne [4]. Pomimo faktu, iż rozstrzygnięcie czy NP = PSPACE wciąż należy do nierozwiązanych problemów informatyki, przyjmuje się, że problemy klasy NP są łatwiejsze.

Dużo miejsca poświęciłem też samemu problemowi weryfikacji modelowej w logice LNC. Weryfikacja modelowa – w skrócie – metoda sprawdzania poprawności programu komputerowego i jego zgodności z wymaganiami. Zazwyczaj taka weryfikacja polega na przygotowaniu zestawu testów, które powinny sprawdzić poprawność wykonania programu w określonych warunkach. Problem w tym, że z definicji testy nie sprawdzają, czy błędów nie ma, a jedynie czy udało się je znaleźć.

Metoda weryfikacji modelowej działa inaczej. Rozpatrywany system lub program reprezentowany jest w postaci modelu – zazwyczaj struktur Kripkego (grafy skierowane). Wykonanie programu jest jednym z możliwych przebiegów w modelu, natomiast wymagania są zdefiniowane w postaci formuł w logice temporalnej. Formuły analizują cały model i wszystkie jego możliwe przebiegi, a więc wszystkie możliwe scenariusze wykonania programu. W teorii powinna być to kompleksowa metoda, skuteczniejsza niż pokrywanie kodu testami, które działają punktowo. Tyle tylko, że metoda weryfikacji modelowej jest tak dobra, jak dobry jest weryfikowany model. Konwersja programu do modelu może być niepełna, uproszczona lub zawierać błędy, zwłaszcza w przypadku bardziej złożonych systemów. Innym problemem jest też rozmiar modelu i złożoność formuł weryfikujących. Dla dużych problemów, ze względu na wykładniczą złożoność, jest to metoda nieefektywna, choć –jak już wspomniałem – w przypadku logiki LNC klasa złożoności problemu jest niższa.

Dodatkowo zauważyłem, że formuły w logice LNC – czyli element weryfikujący – same mogą zostać rozwinięte do postaci struktur Kripkego. Można więc te formuły uznać za wykonywalną specyfikację wymagań. Działa to tak, że definiujemy zachowanie systemu w postaci formuł logicznych LNC, a następnie na bazie wynikowej formuły tworzony jest model, co do którego mamy pewność, że spełnia wymagania. Oczywiście – pozostaje jeszcze kwestia interpretacji modelu i jego odwrotnej konwersji na faktyczny program.

To tak w skrócie (śmiech).

A czemu właśnie ten obszar w pracy?

Jak wspominałem wcześniej – profesor Mulawka kierował Zakładem Sztucznej Inteligencji. Systemy logiczne zalicza się do metod AI. Profesor, w ramach poszerzania horyzontów, wręczył mi monografię dr Świętorzeckiej, w której została zaproponowana logika LNC. Jako że lubię matematykę nie mniej niż informatykę, a metody AI oparte na systemach logicznych są na pograniczu obu tych dziedzin, to stwierdziłem, że jest to obszar, którym chciałbym się zainteresować.

Warto było. Udało się opracować i zaimplementować algorytmy, które w porównaniu z dostępnymi wtedy odpowiednikami dla logiki LTL działały – w zależności od poziomu skomplikowania formuły lub modelu – nawet do kilku tysięcy razy szybciej. To całkiem dobry wynik. Dodatkowo mogły operować na dużo większych formułach i dużo większych modelach.

No, to wiemy, dlaczego logiki temporalne. A dlaczego w ogóle informatyka? Z matematycznego zainteresowania?

W jednej z książek przeczytałem kiedyś, że informatyka to matematyka w praktyce. Podpisuję się pod tym stwierdzeniem. Szczerze, to nie wiem, czy kiedykolwiek zastanawiałem się, czy iść na informatykę. Po prostu wiedziałem. Mam dwóch starszych braci. Kiedy zaczynałem podstawówkę, jeden z nich już pracował jako informatyk. Drugi był na politechnice i kilka lat później też został informatykiem. Oprócz gier – które oczywiście były wtedy najciekawsze – bracia pokazali mi też Pascala i Delphi. Kiedy gry mi się nudziły, próbowałem pisać jakieś proste programy. Więc, gdy kilka lat później na lekcji informatyki pojawił się Logo Komeniusz, byłem gotowy. I chyba też w pewien sposób ustawiony, bo hierarchia przedmiotów w szkole, priorytety, profil klasy w liceum, przedmioty maturalne czy kierunek studiów wydawały mi się zawsze wyborami oczywistymi.

No tak. To jest twoja droga. A jak długo tę drogę realizujesz w Finture? Jak tu trafiłeś?

W Finture jestem od ponad pięciu lat. Ta historia też lekko zahacza o okres akademicki. W Zakładzie Sztucznej Inteligencji, ale też wcześniej w trakcie studiów, miałem styczność z różnymi formami programowania – innymi niż standardowe podejście obiektowo-imperatywne jak w Javie czy C++. Zetknąłem się m.in. z Haskellem, który zmusił mnie do zupełnie innego, bardziej matematycznego spojrzenia na programowanie. Haskell jest językiem czysto funkcyjnym. Programy powstają przez deklaracje i składanie ze sobą funkcji, które same mogą przyjmować lub zwracać inne funkcje. Nie chcę teraz wchodzić w szczegóły funkcyjnego paradygmatu programowania, niemniej zupełnie inaczej pisze się programy, gdy np. nie można zadeklarować zmiennej. Było to coś, co mnie wtedy bardzo zainteresowało, może nawet zafascynowało.

W 2012 roku na portalu Coursera trafiłem na kurs „Functional Programming Principles in Scala” Martina Odersky’ego, twórcy języka Scala. Po kursie, który oczywiście polecam, zainteresowałem się tym językiem – przedstawianym jako bardziej zwięzła Java na sterydach – który, czerpiąc z Haskella, łączy paradygmaty programowania obiektowego i funkcyjnego. Język spodobał mi się na tyle, że oprogramowanie na potrzeby doktoratu zacząłem – i finalnie skończyłem – implementować w Scali. Jednocześnie zacząłem szukać pracy i projektów pod kątem tego języka, co nie było łatwe, bo nie był on w tamtym czasie specjalnie popularny. I tu pojawia się Finture, który taką ofertę pracy miał.

I cały ten czas pracujesz w zespole dla jednego klienta?

Tak, od 5 lat jestem w tym samym projekcie. Dodatkowo kilka miesięcy temu został powołany w Finture zespół RND (Research and Development), którego jestem członkiem. W ramach tego zespołu pracujemy nad standaryzacją procesu wytwarzania oprogramowania, wspieramy inne zespoły w kwestiach technologicznych, budujemy bazę wiedzy oraz badamy perspektywiczne obszary innowacji, głownie generatywne AI. Jednak zdecydowana większość mojej pracy to praca na projekcie.

Od początku budujesz projekt?

I tak i nie, zależy który system. Dołączyłem do zespołu, kiedy główna aplikacja działała już produkcyjnie. Do moich obowiązków należało utrzymanie systemu, dodawanie nowych funkcjonalności, usuwanie starych oraz refactoring, również głęboki. Jednym z pierwszych większych zadań było przepisane całego front-endu na Reacta i Reduxa. Była to żmudna, aczkolwiek satysfakcjonująca, praca. Finalnie udało się zredukować liczbę linii kodu o około połowę przy jednoczesnym dodaniu kilku nowych funkcjonalności. Zakres moich obowiązków zmieniał się w czasie. Oprócz zadań ściśle developerskich zacząłem uczestniczyć w procesie formułowania wymagań oraz projektowania wysokopoziomowej architektury, następnie pojawiły się zagadnienia z obszarów DevOps, Cloud czy BigData a także zarządzanie pracą zespołu developerskiego, który rozrósł się w międzyczasie. W tym momencie można chyba powiedzieć, że jestem liderem technicznym, głównym programistą i architektem. To dość duży obszar kompetencji, którym w pewnym momencie będę się chciał, a nawet musiał, podzielić. Na razie – choć to też się powoli zmienia – pracujemy w startupowej atmosferze: zespół jest mały, każdy jest trochę od wszystkiego, a rzeczy dzieją się szybko i dynamicznie.

Trzeba szybko reagować?

Czasami. Mi to odpowiada. Nie nudzę się. Oczywiście, jak zawsze, są dobre i złe strony takiego podejścia. Dla mnie jednak, na chwilę obecną, zalety przeważają nad wadami. Rozwój – zarówno mój jak i systemów – jaki miał miejsce przez te 5 lat, jest ogromny. Raczej nieporównywalny do innych projektów, w których uczestniczyłem. Do tego dochodzi bardzo duża dowolność w doborze technologii i projektowaniu rozwiązań. Nasze „zwinne” podejście sprawia, że czasami pomysł na feature lub usprawnienie i jego wdrożenie dzieli zaledwie kilka godzin.

To faktycznie zwinne.

Szybko, ale bezpiecznie. Pomimo niskiego time-to-delivery nie pracujemy w trybie „studenckiego projektu na noc przed oddaniem”. Zdaję sobie sprawę, że brawura może się łatwo skończyć katastrofą. Każdy senior developer – w tym ja – ma prawdopodobnie na swoim koncie szybką wrzutkę, która położyła produkcję. Dlatego też stosujemy wobec siebie samych zasadę ograniczonego zaufania, odpowiednio planujemy i korzystamy z wypracowanych rozwiązań i metod, które zapewniają odpowiednią jakość oraz – jeżeli zaszłaby taka potrzeba – umożliwiają szybkie wycofanie zmian.

Brzmi to wszystko trochę tak, jakbyś poza pracą niewiele miał czasu na inne rzeczy…

Nie zawsze tak jest, ale zdarza się, tym bardziej, że granie w Pull The Wire to też już trochę praca. Jeśli nie pracuje, to prawdopodobnie jestem na koncercie lub w busie w drodze na koncert, z którego czasami też pracuję. Czasami zdarzają się jeszcze gry komputerowe. Aktualnie gram – jak zapewne większość moich kolegów – w Diablo IV.

Diablo to tak z sentymentu?

W jakimś stopniu na pewno. Tym bardziej, że twórcy puszczają oko do starszych graczy. Nowe Diablo dosłownie gra na nostalgii, gdy słyszy się motyw gitarowy z Tristram z pierwszej części.

Zaczęliśmy od muzyki i na muzyce kończymy. Dzięki!

[1] Nagroda publiczności za występ na festiwalu Pol’and’Rock. Pull the Wire w 2023 zagra na Dużej Scenie festiwalu 5 sierpnia.

[2] Noraebang – koreańskie „pokoje do śpiewania”, wyciszone, z całym potrzebnym sprzętem do karaoke, które można wynająć wraz ze znajomymi.

[3] Klasa NP jest zbiorem wszystkich problemów decyzyjnych, które mogą̨ być rozwiązane przy pomocy niedeterministycznej maszyny Turinga w wielomianowym czasie.

[4] Klasa PSPACE jest zbiorem wszystkich problemów decyzyjnych, które mogą być rozwiązane przy pomocy deterministycznej maszyny Turinga przy użyciu wielomianowej ilości pamięci.