Plurrrr

Since the release of systemd in 2010 the project has been getting a continuous and steady stream of new features and added capabilities. With a code count of more than 1.3 million lines of code, where Lennart Poettering has just added yet another 20.000 new lines of code with the merge of his personal systemd-homed git tree into systemd, and with a continuous open issue counter at about 1.400 issues, where new issues and bugs keep popping up, systemd should be considered experimental and not safe to run anywhere.

When GHC 9.2 was released in late 2021, I was eager to migrate my projects, particularly to reap the ergonomic benefits of the record dot syntax feature. My disappointment was immeasurable as I discovered that some of my more involved type-level computations caused GHCi to get stuck, just spinning indefinitely at full CPU load – it meant that in order to get productive with the new compiler, I would have to invest a potentially significant amount of time to debug a regression. Since my plate was already full at the time, I postponed this with the hope of an upcoming minor release magically fixing the issue.

We all know that we can use Haskell to write functional programs that compute stuff. But can we also use Haskell to write mathematical proofs? Yes! In case you have never been exposed to dependent types, the concept of writing proofs with a programming language will surely sound alien to you. In this blog I hope to give you an informal introduction to dependent types in Haskell that will allow you to understand what does it mean to prove something in Haskell and how to do it. I strongly recommend that you follow along with ghci on your side.