Posts

Earthquake near Basel!
Well that was wild! I was sitting in bed when it suddenly started wobbling from side to side. My first thought was that the fan had made it shake, but that didn’t really make sense in terms of the amount of shaking that was going on.
Sat, 10 Sep 2022
Type You an Idris – Part 1: Warmup
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.
Fri, 2 Sep 2022
Applying for a UK EHIC
With Brexit, etc. health insurance when travelling has gotten a bit complicated and the application process is slightly confusing. So I thought I’d document my experience.
Tue, 24 May 2022
A Crash Course in Sequencing IO Functions
Intro This is yoinked from an answer I gave on the Idris2 discord where someone was confused about using IO when there was multiple functions involved. I’ve slightly restructured it, but it’s still basically the Discord answer verbatim.
Fri, 25 Mar 2022
An attempt at explaining Decidable Equality
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.
Tue, 15 Mar 2022
Happy Swiss Siren Day!
It’s the first Wednesday of February. If you’re Swiss, y’all know what that means!…
Wed, 2 Feb 2022
Booting via the UEFI Shell
After having the motherboard replaced in my laptop, I was unable to reconfigure the boot-manager to rEFInd the normal way. Fortunately, I had a tiny bit of experience with the UEFI shell and ‘recovered’ things through that.
Fri, 6 Aug 2021
Recovering From a Broken Smartcard
My Nitrokey suddenly broke. This is some ramblings about working my way through the harebrained backup schemes I established, and setting up something a bit more sane+safe…
Wed, 28 Jul 2021
Implementing Condition Variables in Racket
Explaining and implementing Birell’s 2003 paper on Condition Variables for Modula-2+, in Racket.
Tue, 27 Jul 2021
Cross-Compiling Splash-3
Cross-compiling can be a bit difficult to put it mildly. This should hopefully be straightforward to follow and help you if you’re looking to cross-compile Splash-3 for use with gem5 or a similar simulator.
Wed, 10 Mar 2021