In this post we’ll tackle the following puzzle:

We are given two arrays, one with adjectives and another one with nouns . A combined list is which is the Cartesian product between the two arrays. We want to build a performant way to get specific a subarray of of arbitrary size at a specific page.

Continue reading “Performant implementation of pagination on Cartesian products” →

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.

Continue reading “Towards Hoare logic for a small imperative language in Haskell” →

This post was generated from a literate Haskell file.

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

Continue reading “Advent of Code #13” →

DST changes in North Macedonia on the last Sunday of October. It happens to be the 25th of October this year.

What can we do with the previous statement, other than generalize it and try to prove a mathematical fact about it? 🙂

Continue reading “Proof: One Sunday every 7 days” →