During my time in Arend, I was reading the “Programming Language Foundations in Agda” book to refresh my knowledge of theorem proving. To actually learn something, you need to get your hands dirty, so I was rewriting the code snippets in Arend. The book is a collection of Markdown files with code snippets in Agda, and by adding Arend snippets alongside the original ones, I was creating a version of PLFA where you can compare the same proofs in different languages.

Last December was the first time I seriously participated in AoC. I generally had a lot of fun solving the tasks, earning ⭐s, discussing solutions with my friend, and even peeking into r/adventofcode a bit when I was stuck. Probably, the main thing AoC reminded me about was “be practical, Steve”.

If you want to get to the leaderboard, or don’t want to read about elves and Christmas trees in January and February, you have only one day to solve two tasks. AoC only wants you to give the answer, not the solution, so it doesn’t really matter if your solution is super optimal or nicely coded. All this hints that one should take a very practical approach: start with the most obvious and simple solution, and try to improve it only when it doesn’t work.