LLM (Large Language Model) powered AI (Artificial Intelligence) assistants are a popular tool used by programmers, but what impact do they have? In this thesis we investigate two such tools designed by JetBrains: AI Assistant and FLCC (Full Line Code Completion).
We collected over 40 million actions - including editing, code executions, and typing - in the form of metric data spread out over 26 thousand users. With this data, we look at how user behavior changes when assisted by AI Assistant or FLCC.

Users spent more time in their IDEs (Integrated Development Environment) and typed more when assisted. In most cases, we see a decline in (manual) testing, or at best an equivalent level. And how do multi-programming language benchmarks reflect acceptance rates by users for these respective languages? There seems to be no real correlation between these benchmark results and what users accept in their generations, but the available benchmarks are also limited.

In the end, more research is required to put these results in perspective, for now, it is still up in the air whether the changes in user behavior are positive or negative. But relating this to existing works the impact seems mostly positive on users of AI Assistant and FLCC.

Agda allows for writing code that can be mathematically proven and verified to be correct, this type of languages is generally known as a proof assistant. The agda2hs library makes an effort to translate Agda to readable Haskell, in a way the Haskell is still consistent. In previous work it is shown that with the current agda2hs implementation, rudimentary structures can be translated to Haskell from Agda with agda2hs. In this paper the translation and verification of infinite structures to readable Haskell code is researched. This allows for future work to be done on verification of more complex libraries because the concept of infinite structures is used often in Haskell. The results of the research were that translation of rudimentary infinite structures is possible, but functions creating infinite structures cannot be translated at this point in time.