Introduction
When I was trying to pick a topic for my master’s thesis, I couldn’t decide between something practical or more research-focused. In the end, I chose a research-based topic because I figured I’d get plenty of practical experience after school anyway. Three classes really stood out to me: Database Systems, Programming Distributed Systems with Elixir, and Functional Programming with Haskell. The first two felt more hands-on and something I’d keep learning on the job, so I went with Functional Programming, especially verified functional programming. It opened up a fresh perspective for me and felt like a unique skill set to add to my toolkit.
After three years in the industry, I’m pretty sure typing systems and testing are key to building reliable software. Lately, I’ve been diving into Functional Programming (check out Functional Programming made easy) and found some neat principles that help write better code. Stuff like pure functions, higher-order functions, polymorphism, and immutability are super helpful across many languages. Then there are cool features like algebraic types, Monads, and lazy evaluation that are more unique to functional languages. Overall, it’s a solid way among other things to make programs more reliable and easier to manage.
Combining functional languages with powerful type systems like dependent or refinement types really levels things up. What’s cool is that you can write programs that are literally proven to work—no guesswork. Instead of just saying a sorting function takes a
list of ints and returns a list of ints, you specify it returns a sorted list. The type system is so smart that if your code passes, it’s guaranteed to behave right, meaning you might not even need unit tests. Plus, dependent types let you link inputs and outputs in neat ways, like ensuring the sorted list has exactly the same elements as the input, not some random sorted array. It’s like having built-in proof your program’s solid!My thesis is all about diving into LiquidHaskell, which is basically an awesome extension to Haskell that lets you do verification right in your code. By just adding some annotations to the usual type system, you can automatically prove various properties about your Haskell programs. I'm focusing on Priority Queues, using LiquidHaskell to prove that different Priority Queue implementations are actually correct. What’s cool is that the code and proof aren’t separate — they’re combined into one neat program.
Planning
I have already gathered the initial knowledge as I was writing my seminar. Additionally, I have built solid project structure backed with nix for both the code and latex provided in this repository.