Towards Hoare logic for a small imperative language in Haskell

Recently I finished Logical Foundations, and I have to admit it was an excellent read. This post is directly inspired by the Simple Imperative Programs section of the same book.

What is an imperative programming language? Well, nowadays they run the world. C, Python, JavaScript, PHP – you name it – we all write code in them using imperative style; that is, we command the computer and tell it what to do and how to do it. The mathematical language is very unlike this – it is more declarative rather than imperative – it doesn’t care about the how.

I’ve always been fascinated by mathematical proofs, especially the mechanical part around them because computers are directly involved in this case. Hoare logic is one of those systems that allows us to mechanically reason about computer programs.

We will implement a small imperative language together with (a very simple) Hoare Logic that will allow us to reason about programs in this imperative language.

Advent of Code #13

This post was generated from a literate Haskell file.

In this post, we’ll tackle the 13th problem of AoC2020, Shuttle Search.

Haskell memoization and evaluation model

I am tackling the Advent of Code challenges in Haskell. In particular, Advent of Code #10 was fun (spoilers clicking on that link, but no spoilers in this blog post itself). Part two required using memoization to be solved, and I had already used memoization in other programming languages but not in Haskell. So I learned the hows and the whys of memoization in Haskell – thus the reason why this article exists.

In order to learn about memoization in Haskell, I did a quick Google and it led me the Memoization article on the Haskell Wiki. That article is good, but it only explains the how, not the why. I will cover both how and why in this blog post.

Advent of Code #8

This post was generated from a literate Haskell file.

In this post we’ll tackle the 8th problem of AoC2020, Handheld Halting.

Diversity and Bias

I just finished the Psychology of Diversity and Unconscious Bias Udemy course. It was an excellent course with explanations that were clear and backed by science papers, so I enjoyed it. In this post I will write an overview of the course.