Thomas Ekström Hansen
Thomas Ekström Hansen
Home
Recent posts
Experience
Accomplishments
Blog
Coursework
Light
Dark
Automatic
Posts
Writing a PRNG using ChatGPT
What do you do if you need a pseudorandom number generator but don’t know anything about how to implement that and, crucially, don’t care how good it is? You
could
read some papers, but ChatGPT had been making waves for a while, so why not try that?
Thomas Ekström Hansen
Thu, 16 Mar 2023
Dai Station: an Idris Constraint Solver
As part of my Ph.D. exploration on how we know the types we’re using model what we think they do, I decided to try to implement a constraint solver in Idris (technically Idris2, but Idris1 is deprecated at this point, so I use ‘Idris’ and ‘Idris2’ interchangeably).
Thomas Ekström Hansen
Thu, 16 Feb 2023
Booting from a USB on an Odroid N2
If you’ve flashed an ISO to a USB-drive rather than the boot card of your SBC, is there any way to load the thing? Yes, but it requires a bit of digging around in a weird pre-boot environment…
Thomas Ekström Hansen
Thu, 15 Dec 2022
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.
Thomas Ekström Hansen
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.
Thomas Ekström Hansen
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.
Thomas Ekström Hansen
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.
Thomas Ekström Hansen
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.
Thomas Ekström Hansen
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!…
Thomas Ekström Hansen
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.
Thomas Ekström Hansen
Fri, 6 Aug 2021
«
»
Cite
×