idris2

The best way to learn & understand a thing is to implement it. So let’s implement (a subset) of Idris2! This part is an introduction and covers some function exercises that will help later.

One of the more difficult concepts in Idris, I’ve found, is proving things through dependent types. The ‘simplest’ introduction to this is probably the DecEq interface, which this post aims to introduce, explain, and implement.

Explaining and implementing Birell’s 2003 paper on Condition Variables for Modula-2+, in Racket.

A dive into functional concurrency, FFIs, and thread weirdness.