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
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
It's the first Wednesday of February. If you're Swiss, y'all know what that means!...
Wed, 2 Feb 2022
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
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
Explaining and implementing Birell's 2003 paper on Condition Variables for Modula-2+, in Racket.
Tue, 27 Jul 2021
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
A dive into functional concurrency, FFIs, and thread weirdness.
Wed, 24 Feb 2021
A step-by-step guide to dualbooting encrypted Windows and Arch Linux, using the rEFInd boot mananger.
Sun, 12 Jan 2020
A detailed overview of how I installed Arch Linux on my Lenovo ThinkPad X1 Extreme (Gen 1), having never install Arch before.
Thu, 17 Jan 2019