Kod w pracy, rytm po godzinach
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?
Z perkusją zetknąłem się około 13. roku życia. Początkowo chciałem grać na gitarze, ale w mojej miejscowości był tylko jeden nauczyciel i trudno było się do niego dostać. Czekając kiedyś w Gminnym Ośrodku Kultury na jego zajęcia z innym uczniem, spróbowałem zagrać na stojącej na scenie perkusji. No i tak już zostało.
Teoretycznie gram około 22 lat, choć w praktyce miałem kilka dłuższych przerw, m.in. podczas Erasmusa, rocznego wyjazdu do Korei czy w czasie studiów i doktoratu.
Dużo czasu musisz poświęcać na granie i ćwiczenie?
Kiedyś trenowałem znacznie więcej. Dziś – głównie z powodów zawodowych i zespołowych – mam na to mniej czasu. Zdarzają się okresy, gdy ćwiczenia ograniczają się właściwie do przygotowań do koncertów, a praca nad techniką schodzi na dalszy plan, nad czym trochę ubolewam.
Korea od środka – praca, kultura i noraebangi
Wspomniałeś coś o służbowym wyjeździe do Korei…
Byłem wtedy zatrudniony w Samsungu i wziąłem udział w programie Global Mobility – półrocznej lub rocznej wymianie pracowniczej między centralą w Korei a zagranicznymi oddziałami firmy.
Wyjazd wspominam bardzo dobrze. Najciekawsze było poznawanie kraju oraz odmiennej kultury pracy. Pracowałem przy tym samym projekcie co wcześniej, więc zakres obowiązków się nie zmienił, ale inny był sposób ich realizacji – od doprecyzowywania wymagań po prezentowanie i dokumentowanie wyników.
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!
Doktorat między koncertami – nauka po godzinach
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ą i do dziś biorę taki scenariusz pod uwagę, choć nie wiem jeszcze, czy bardziej interesowałaby mnie praca naukowa, czy dydaktyczna.
Promotorem moich wcześniejszych prac był prof. Jan Mulawka, który zaproponował mi doktorat w Zakładzie Sztucznej Inteligencji na Wydziale Elektroniki i Technik Informacyjnych. Ponieważ już wcześniej myślałem o doktoracie, nie zastanawiałem się długo – tym bardziej, że pracę inżynierską i magisterską pisało mi się pod jego opieką bardzo dobrze. Wydawało mi się, że z doktoratem będzie podobnie. Jak się później okazało – myliłem się. (śmiech)
Logika temporalna i weryfikacja modelowa
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?
W swojej pracy doktorskiej zajmowałem się logiką LNC (Logic Next Change), która jest specyficznym fragmentem logiki LTL opartej na dyskretnej i liniowej strukturze czasu. LNC to pełny system logiczny zaproponowany przez dr hab. Kordulę Świętorzecką. Początkowo badałem możliwość implementacji maszynowej rachunku LNC, czyli stworzenia systemu umożliwiającego automatyczne wnioskowanie w tej logice.
Z czasem zauważyłem, że LNC jest podzbiorem logiki LTL, ale ma interesujące właściwości. Kluczowa część mojej pracy polegała na wykazaniu, że dwa podstawowe problemy analizowane w logikach temporalnych – problem spełnialności oraz problem weryfikacji modelowej – są dla LNC problemami NP-zupełnymi, podczas gdy dla pełnej logiki LTL należą do klasy PSPACE-zupełnych. Ponieważ w praktyce przyjmuje się, że problemy z klasy NP są łatwiejsze obliczeniowo, ma to istotne znaczenie.
Dużą część badań poświęciłem weryfikacji modelowej, czyli metodzie sprawdzania poprawności programów względem określonych wymagań. W przeciwieństwie do klasycznego testowania, które sprawdza tylko wybrane przypadki, weryfikacja modelowa analizuje cały model systemu (najczęściej w postaci struktur Kripkego) oraz wszystkie możliwe przebiegi jego działania.
Zauważyłem też, że formuły w logice LNC mogą zostać rozwinięte do postaci struktur Kripkego, co pozwala traktować je jako wykonywalną specyfikację wymagań: z formuł logicznych można wygenerować model systemu, który z definicji spełnia zadane warunki.
A czemu właśnie ten obszar w pracy?
Zainteresowałem się logiką LNC dzięki prof. Janowi Mulawce, który zaproponował mi monografię dr Korduli Świętorzeckiej. Połączenie matematyki, informatyki i metod AI wydało mi się szczególnie interesujące. W efekcie opracowałem algorytmy, które w porównaniu z rozwiązaniami dla logiki LTL działały nawet kilka tysięcy razy szybciej i obsługiwały większe modele.
Od matematycznej ciekawości do pracy w Finture
No, to wiemy, dlaczego logiki temporalne. A dlaczego w ogóle informatyka? Z matematycznego zainteresowania?
Informatyka to – jak kiedyś przeczytałem – matematyka w praktyce i w pełni się z tym zgadzam. Właściwie nigdy nie zastanawiałem się, czy iść w tym kierunku. Mam dwóch starszych braci – jeden już pracował jako informatyk, gdy zaczynałem szkołę podstawową, drugi studiował na politechnice i także został informatykiem. Pokazali mi nie tylko gry, ale też Pascala i Delphi, więc gdy gry się nudziły, próbowałem pisać proste programy. Dlatego, gdy później na lekcjach pojawił się Logo Komeniusz, byłem już na to przygotowany, a kolejne wybory edukacyjne były dla mnie dość oczywiste.
No tak. To jest twoja droga. A jak długo tę drogę realizujesz w Finture? Jak tu trafiłeś?
W Finture pracuję od ponad pięciu lat. Jeszcze podczas studiów i w Zakładzie Sztucznej Inteligencji zetknąłem się z różnymi podejściami do programowania, m.in. z Haskell, który wymaga bardziej matematycznego spojrzenia na kod i opiera się na paradygmacie czysto funkcyjnym. To doświadczenie bardzo mnie zainteresowało.
Później trafiłem na kurs „Functional Programming Principles in Scala” prowadzony przez Martin Odersky na Coursera. Dzięki niemu poznałem Scala – język łączący programowanie obiektowe i funkcyjne, często określany jako bardziej zwięzła „Java na sterydach”. Zainteresował mnie na tyle, że oprogramowanie do mojego doktoratu napisałem właśnie w Scali. Równolegle zacząłem szukać pracy związanej z tym językiem – i w ten sposób trafiłem do Finture.
I cały ten czas pracujesz w zespole dla jednego klienta?
Od pięciu lat pracuję przy tym samym projekcie. Kilka miesięcy temu w Finture powstał też zespół R&D, którego jestem członkiem. Zajmujemy się m.in. standaryzacją procesu wytwarzania oprogramowania, wsparciem technologicznym innych zespołów, budowaniem bazy wiedzy oraz analizą nowych obszarów – głównie generatywnego AI. Nadal jednak większość mojego czasu zajmuje praca projektowa.
Zwinność działania i szybkie wdrażanie pomysłów
Od początku budujesz projekt?
Dołączyłem do zespołu, gdy główna aplikacja była już na produkcji. Początkowo zajmowałem się jej utrzymaniem, dodawaniem nowych funkcjonalności oraz refaktoryzacją. Jednym z pierwszych większych zadań było przepisanie całego front-endu na Reacta i Reduxa, co pozwoliło zmniejszyć liczbę linii kodu o około połowę i jednocześnie dodać nowe funkcje.
Z czasem mój zakres obowiązków rozszerzył się o udział w definiowaniu wymagań, projektowanie architektury oraz obszary DevOps, Cloud i Big Data, a także koordynację pracy zespołu developerskiego. Dziś pełnię rolę technicznego lidera i architekta, choć nadal pracujemy w dość startupowej, dynamicznej atmosferze.
Trzeba szybko reagować?
Czasami, ale mi to odpowiada – dzięki temu się nie nudzę. Jak w każdym podejściu są plusy i minusy, jednak na razie zdecydowanie przeważają zalety. Przez te 5 lat zarówno ja, jak i rozwijane systemy bardzo się rozwinęliśmy, w tempie większym niż w innych projektach, w których uczestniczyłem. Dodatkowym atutem jest duża swoboda w doborze technologii i projektowaniu rozwiązań – w naszym zwinnym podejściu od pomysłu na usprawnienie do wdrożenia czasem mija 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 stosujemy zasadę ograniczonego zaufania. Planowanie i sprawdzone metody pomagają utrzymać jakość oraz w razie potrzeby szybko wycofać zmiany.
Między kodem a muzyką
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.