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.

I finished the first chapter (out of three) and put it on hold for quite some time. It was just a personal project that very few people knew about. But this April, to my great surprise, I was contacted by Philip Wadler, the author of PLFA. One of the former members of the Arend team mentioned my project to Professor Wadler, and he suggested mentioning it on the book’s website as a derived work! You can find it there now!

Not gonna lie, this made me very happy. It is not often that your small personal project gets this kind of recognition from a famous person. This could be the highest achievement in my failed career as a scientist 😂 Even before this, I was thinking about doing some theorem proving in my spare time just because I like it. But now I am even more motivated. I should finish PLFArend — there are two chapters ahead!