Finture_Heroes_05

Temporal logics, functional programming, and percussion. Marek Adamek, Custom Software Developer at Finture, shares his passions, works, and projects. After hours, he is a punk rock drummer for the band 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?

The first time I encountered drums was around the age of 13, during the early years of junior high school. Originally, I wanted to play the guitar, but in my town, there was only one guitar teacher, and he was always busy. I remember waiting at the Municipal Cultural Center until he finished a lesson with someone else. There happened to be a drum set on the stage. I gave it a try – and that's how it stayed. I never had guitar lessons then or later.

Simple arithmetic would suggest that I've been playing for... 22 years, but that's not entirely true. I had quite long breaks for various reasons: once it was Erasmus, another time a year-long business trip to Korea, another time university and a doctorate, or other matters that knocked me out of – rhythmically speaking – the rhythm.

How much time do you have to dedicate to playing and practicing?

I used to practice more. Now, due to professional and band-related reasons, I have less time for it. There are periods when exercises are limited to preparations for concerts, and playing is focused on performing those concerts. Polishing my technique takes a back seat, which I regret.

You mentioned something about a business trip to Korea...

Yes, I was employed at Samsung at that time, where I participated in the Global Mobility program. It involved six-month, one-year, or two-year employee exchanges between the headquarters in Korea and branches in other countries, somewhat similar to the Erasmus program.

I remember this trip very well. The most interesting part was getting to know the country and its culture, including work culture, which was significantly different from what I knew in Poland. It was particularly intriguing because, before and during the trip, I was involved in the same project. The scope of my duties didn't change much, but the way they were performed did, from specifying requirements to presenting and documenting results.

The emotions that accompanied me at various stages of the stay were also interesting – from fascination at the beginning, through surprise, incomprehension, moments of frustration, to, ultimately, acceptance.

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!

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?

At that time, I was considering an academic career, and to some extent, I still contemplate such a scenario. Whether it would be more focused on research or teaching, I don't know; preferences change over time.

The supervisor for my earlier diploma theses was Professor Jan Mulawka, and it was he who proposed a Ph.D. for me in the Department of Artificial Intelligence at the Faculty of Electronics and Information Technology. Since I had been considering a Ph.D. earlier, I didn't hesitate for long. Especially since my engineering and master's theses were smooth, fast, and enjoyable under his guidance. I thought it would be the same with the Ph.D. – as it turned out later, I was mistaken (laughter).

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?

Temporal logics are, in short, an extension of classical logic. In these logics, additional operators are distinguished, allowing the definition of logical formulas that take into account time and reasoning with their use. Such operators include, for example, "next," "always," "sometime," "until." With their help, it is possible to describe changes in the values of logical propositions over time. Temporal logics, compared to classical logic, have greater expressive power. In such logic, more can be expressed.

There are many temporal logical systems. In my work, I examined the Logic Next Change (LNC), which is a specific fragment of Linear Temporal Logic (LTL) based on a discrete and linear time structure.

LNC is a complete logical system proposed by Dr. Kordula Świętorzecka. Initially, my research focused on the possibility of implementing a machine calculus for LNC, a system that would enable reasoning in this logic. However, the more I examined LNC, the more it reminded me of Linear Temporal Logic (LTL), about which it seems everything has already been said and written in the field. And I was right. LNC turned out to be a subset of the LTL calculus, but one with very interesting properties.

The main part of my Ph.D. involved demonstrating that two fundamental problems considered in the case of temporal logics – namely, the satisfiability problem and the model-checking problem – are NP-complete problems for LNC [3], whereas for the full Linear Temporal Logic (LTL), they are PSPACE-complete problems [4]. Despite the fact that determining whether NP = PSPACE remains an unresolved problem in computer science, it is generally accepted that problems in the NP class are considered easier.

I also dedicated a significant portion of my work to the model-checking problem in LNC logic. Model checking, in short, is a method for verifying the correctness of a computer program and its compliance with requirements. Typically, this verification involves preparing a set of tests intended to check the correctness of program execution under specific conditions. The issue here is that, by definition, tests do not verify whether there are no errors; they only determine whether errors, if any, have been found.

The model-checking method operates differently. The considered system or program is represented in the form of a model – typically Kripke structures (directed graphs). The execution of the program is one of the possible paths in the model, while the requirements are defined in the form of formulas in temporal logic. The formulas analyze the entire model and all its possible paths, meaning all possible execution scenarios of the program. In theory, this should be a comprehensive method, more effective than code coverage with tests, which operate pointwise. However, the model-checking method is only as good as the verified model. The conversion of the program into a model may be incomplete, simplified, or contain errors, especially for more complex systems. Another problem is the size of the model and the complexity of the verifying formulas. For large problems, due to exponential complexity, this method is inefficient, although, as mentioned before, in the case of LNC logic, the complexity class of the problem is lower.

Additionally, I noticed that formulas in LNC logic – the verification elements – can themselves be expanded into the form of Kripke structures. Therefore, these formulas can be considered as an executable specification of requirements. The process works by defining the system's behavior in the form of LNC logical formulas, and then, based on the resulting formula, a model is created. We can be certain that the model satisfies the requirements. Of course, there is still the issue of interpreting the model and its reverse conversion into the actual program.

That's it in a nutshell (laughter).

And why specifically this area in your work?

As I mentioned earlier, Professor Mulawka led the Department of Artificial Intelligence. Logical systems fall under the methods of AI. As part of broadening my horizons, Professor Mulawka handed me a monograph by Dr. Świętorzecka, in which the LNC logic was proposed. Since I enjoy mathematics as much as computer science, and AI methods based on logical systems lie at the intersection of both fields, I concluded that this is an area I would like to explore.

It was worth it. I managed to develop and implement algorithms that, compared to the available counterparts for LTL logic at that time, worked – depending on the complexity level of the formula or model – even up to several thousand times faster. That's quite a good result. Additionally, they could operate on much larger formulas and much larger models.

Well, now we know why temporal logics. But why computer science at all? Is it from a mathematical interest?

In one book, I read once that computer science is mathematics in practice. I stand by that statement. Honestly, I don't know if I ever wondered whether to pursue computer science. I just knew. I have two older brothers. When I started elementary school, one of them was already working as a computer scientist. The other was at the university, and a few years later, he also became a computer scientist. Apart from games – which were, of course, the most interesting at the time – my brothers also introduced me to Pascal and Delphi. When I got bored with games, I tried to write some simple programs. So, when a few years later Logo Komeniusz appeared in my computer science class, I was ready. And I guess in a way, I was predisposed because the hierarchy of subjects in school, priorities, the class profile in high school, subjects for the final exams, or the choice of university major always seemed like obvious decisions to me.

Yes, that's your path. How long have you been on this journey with Finture? How did you end up here?

I've been with Finture for over five years. This story also slightly intersects with my academic period. In the Department of Artificial Intelligence, but also earlier during my studies, I had experience with various forms of programming – different from the standard object-oriented and imperative approaches like in Java or C++. I encountered, among others, Haskell, which forced me to adopt a completely different, more mathematical perspective on programming. Haskell is a purely functional language. Programs are created by declaring and composing functions, which can themselves take or return other functions. I don't want to delve into the details of the functional programming paradigm right now, but writing programs is entirely different, for example, when you cannot declare a variable. It was something that really interested me at the time, perhaps even fascinated me.

In 2012, I came across the course "Functional Programming Principles in Scala" by Martin Odersky, the creator of the Scala language, on the Coursera platform. After the course, which I highly recommend, I became interested in Scala – presented as a more concise Java on steroids – a language that, drawing from Haskell, combines object-oriented and functional programming paradigms. I liked the language so much that I started – and eventually completed – implementing software for my Ph.D. in Scala. At the same time, I began looking for jobs and projects related to this language, which wasn't easy because it wasn't particularly popular at that time. This is where Finture comes in, which had a job offer for such a role.

And all this time, have you been working with one client?

Yes, I've been on the same project for 5 years. Additionally, a few months ago, the RND (Research and Development) team was established at Finture, and I am a member of that team. Within this team, we work on standardizing the software development process, support other teams in technological matters, build a knowledge base, and explore prospective areas of innovation, mainly in generative AI. However, the vast majority of my work is still project-focused.

Have you been involved in building the project from the beginning?

Yes and no, it depends on which system. I joined the team when the main application was already in production. My responsibilities included maintaining the system, adding new features, removing old ones, and performing refactoring, including deep refactoring. One of the first major tasks was rewriting the entire front-end to React and Redux. It was a tedious but satisfying job. In the end, we managed to reduce the number of lines of code by about half while simultaneously adding several new features. The scope of my responsibilities changed over time. In addition to strictly development tasks, I started participating in the requirements formulation process and high-level architecture design. Later on, issues from areas such as DevOps, Cloud, Big Data, and team management emerged, as the development team grew in the meantime. At this point, I guess you could say I'm a technical leader, the main programmer, and architect. It's quite a broad range of skills that, at some point, I'll want, and even have to, share. For now – although this is slowly changing too – we work in a startup atmosphere: the team is small, everyone does a bit of everything, and things happen quickly and dynamically.

Do you need to react quickly?

Sometimes. It suits me. I don't get bored. Of course, as always, there are both good and bad sides to such an approach. However, for me, at the moment, the advantages outweigh the disadvantages. The development – both mine and the systems' – that has taken place over these 5 years is enormous. It's rather incomparable to other projects I've been involved in. Additionally, there is a lot of freedom in choosing technologies and designing solutions. Our "agile" approach means that sometimes the idea for a feature or improvement and its implementation are only a few hours apart.

It truly is agile.

Quickly, but safely. Despite the low time-to-delivery, we don't operate in a "student project on the night before the deadline" mode. I realize that bravado can easily end in disaster. Every senior developer – including myself – probably has a quick deployment on their record that caused a production issue. That's why we apply the principle of limited trust to ourselves, plan accordingly, and use established solutions and methods that ensure adequate quality and, if necessary, allow for the quick rollback of changes.

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.

Interesting? Feel free to share!