After reading this article I got excited. Apparently it is possible to create a proof language that is both performant, total and reliable. This is one of the things that drew me to Haskell - the idea that the language and compiler should be able to enforce strict rules of correctness. It does not support dependent types though and therefore cannot prove most theorems. Dependent types allows for value level computations at compile time and makes it possible to constrain types arbitrarily. This is because there is no native types and types are at the same level as values and can be used as values.

Making a game in Haskell

During my vacation I’ve been working on making a game in Haskell called HexTech. It has been really fun and inspiring and I’ve learned a lot of new things. The game is a sort of turn-based strategy game on a hexagonal grid. It is mostly a hobby project and it has taken more time than I wanted, but I have been making steady progress. I’m using several tutorials as a guide: this guide for working with hexagonal grids and this one which really gave me a kick start. A lot of my source is based on a rewrite of that game code.

Fumbling with Functional Programming

I love functional programming. It’s just much more beautiful than imperative programming. The down sides usually comes from wanting things done and access to public libraries. I will argue here why FP is worth the effort and reflect around some of the issues in the communities.

For many programmers functional programming can be seen as nothing more than a curiosity. After all, you can seemingly do the same things with imperative languages like Java or C++. Functional programming is a paradigm first and foremost; not restricted to particular languages. Instead of just making “code that works” you should try to emulate the pure mathematical structure lurking behind every problem. This is not something that comes for free. You have to really understand the problem, but then you can write particularly elegant solutions that you can trust.