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.
Let's start with congratulations – because I saw that you won...?
Thank you! Yes, we won the Golden Goat [1] contest. Last year, we had the pleasure of performing on the Small Stage of the Pol'and'Rock Festival. Our performance was appreciated by the audience, and this year, as winners, we will play on the Main Stage.
You play drums. For how long?
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.
How much time do you have to dedicate to playing and practicing?
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
You mentioned something about a business trip to Korea...
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.
Did you become a K-pop fan?
(Laughter) Yes, the exposure to K-pop was significant and prolonged. I wouldn't say I became a fan, but I don't dislike it either. There were songs that I liked, and from time to time, they play in my head.
Was there a karaoke?
Yes! In Noraebangs [2]. I highly recommend it!
Doktorat między koncertami – nauka po godzinach
Was that the moment when you decided to pursue a Ph.D., or had you already decided on a Ph.D. earlier?
The Ph.D. started earlier and was in progress, although it was put on hold. I began my doctoral studies shortly after completing my master's. The trip to Korea temporarily suspended both percussion and the Ph.D. It was one of the reasons why my doctoral studies took frightfully long, lasting for 6 years.
It can take longer.
I don't deny it; however, in my case, if I wanted both the title and completed doctoral studies, 6 years was the maximum. That's how long it took because I worked on the Ph.D. basically after hours and after concerts.
Actually, then, why a Ph.D.? Out of a desire to delve into a particular area of knowledge or for some other reason?
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
Title of your Ph.D. is Development of Temporal Logic Applications in Computer Science..I admit, for me, a novice – I'm only a year into my computer science studies – it's quite challenging. And I did try to read! Could you provide an overview of what your work is about?
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.
And why specifically this area in your work?
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
Well, now we know why temporal logics. But why computer science at all? Is it from a mathematical interest?
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.
Yes, that's your path. How long have you been on this journey with Finture? How did you end up here?
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 at 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.
And all this time, have you been working with one client?
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
Have you been involved in building the project from the beginning?
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.
Do you need to react quickly?
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.
It truly is agile.
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ą
It sounds like you don't have much time for other things besides work...
Not always, but it happens, especially since playing Pull The Wire is also a bit like work. If I'm not working, I'm probably at a concert or on a bus heading to a concert, where I sometimes also work. Occasionally, I still play computer games. Currently, I'm playing – like probably most of my colleagues – Diablo IV.
Diablo is more of a sentimental choice?
To some extent, for sure. Especially since the creators are giving a nod to older players. The new Diablo literally plays on nostalgia when you hear the guitar theme from Tristram in the first installment.
We started with music, and we end with music. Thanks!
[1] Audience Award for the performance at the Pol'and'Rock Festival. Pull the Wire will play on the Main Stage of the festival on August 5, 2023.
[2] Noraebang – Korean "singing rooms," soundproofed spaces equipped with all the necessary karaoke equipment that can be rented with friends.
[3] The NP class is a set of all decision problems that can be solved by a nondeterministic Turing machine in polynomial time.
[4] The PSPACE class is a set of all decision problems that can be solved by a deterministic Turing machine using a polynomial amount of memory.
