GeistHaus
log in · sign up

Håkon's Diary

Part of Håkon's Diary

stories primary
2026-05-10, Sunday
Show full content
Bouldering

I have been bouldering on-and-off for a few years now. The first few times I heard about bouldering, it seemed very unappealing to me. But, forced by slight social pressure, I tried bouldering back in 2012.

And it was really fun! So, fun it did not even feel like exercising, or at least not how I have previously experienced it. I would be completely focused on the problem, not just trying to endure another set or another lap around some track. Alas, I quickly stopped as life got more busy…

Ten years go by. Life happens, and while I stay somewhat active with hiking, I missed bouldering. But somehow I get started again. A group from work is going, and I join. We climb every Friday, no exceptions. Just what I needed to get back on the wall. It feels like starting completely over, of course. I no longer rember what grades I climbed back in 2012, but I remember making a bit of progress. But this time it takes me a couple of sessions just to send a 5.

7A is the lowest grade with black tags in my gym. The black tagged problems look fun, but thus far they have all seemed impossibly hard.
7A is the lowest grade with black tags in my gym. The black tagged problems look fun, but thus far they have all seemed impossibly hard.

After the first year or so, more busy life stuff happened, and I have been struggling to get a climbing session in every week. But still, I make some progress. Gradually, my forearms have been growing, and my technique has improved. I do not consider myself a good climber, by any stretch of imagination. None the less, I reached an important (for me) milestone today:

I sent my first 7A!

A very modest achievement in the grand scheme of things. Many people can climb a 7A. Even many people who have trained a lot less bouldering than I have. Bouldering is not a source of pride for me. To me, sending a 7A signifies the fact that I havent given up on training. Despite life being busy, I keep going to the gym. For fun and for health!

/diary/2026-05.html#2026-05-10
2026-05-10, Sunday
Show full content
Bouldering

I have been bouldering on-and-off for a few years now. The first few times I heard about bouldering, it seemed very unappealing to me. But, forced by slight social pressure, I tried bouldering back in 2012.

And it was really fun! So, fun it did not even feel like exercising, or at least not how I have previously experienced it. I would be completely focused on the problem, not just trying to endure another set or another lap around some track. Alas, I quickly stopped as life got more busy…

Ten years go by. Life happens, and while I stay somewhat active with hiking, I missed bouldering. But somehow I get started again. A group from work is going, and I join. We climb every Friday, no exceptions. Just what I needed to get back on the wall. It feels like starting completely over, of course. I no longer rember what grades I climbed back in 2012, but I remember making a bit of progress. But this time it takes me a couple of sessions just to send a 5.

7A is the lowest grade with black tags in my gym. The black tagged problems look fun, but thus far they have all seemed impossibly hard.
7A is the lowest grade with black tags in my gym. The black tagged problems look fun, but thus far they have all seemed impossibly hard.

After the first year or so, more busy life stuff happened, and I have been struggling to get a climbing session in every week. But still, I make some progress. Gradually, my forearms have been growing, and my technique has improved. I do not consider myself a good climber, by any stretch of imagination. None the less, I reached an important (for me) milestone today:

I sent my first 7A!

A very modest achievement in the grand scheme of things. Many people can climb a 7A. Even many people who have trained a lot less bouldering than I have. Bouldering is not a source of pride for me. To me, sending a 7A signifies the fact that I havent given up on training. Despite life being busy, I keep going to the gym. For fun and for health!

/diary/2026-05.html#2026-05-10
2026-05-08, Friday
Show full content
TYPES 2026
Skyline of Lindholmen where TYPES 2026 was held. [Zoom in! 🔍 ]
Skyline of Lindholmen where TYPES 2026 was held. [Zoom in! 🔍 ]

This week was TYPES 2026. As usual, TYPES was a nice conference, with lots of likeminded people gathered to discuss type theory. I thought the talks this year held a good level, especially the invited talks. And I got to exchange ideas with new and old friends in the community. Zhili presented our joint work on higher kinded containers.

I stayed in a hotel next to Karlatornet, which is the phallic tower you see above. I quite enjoyed Gothenburg this time around, but did not do much sight-seeing, except for dining excursions and a visit to Backa Boulder. This year’s conference I felt was better paced than previous years, where I have felt that there have been just too many talks, and too busy programme.

Flying back to Bergen tonight.

/diary/2026-05.html#2026-05-08
2026-05-08, Friday
Show full content
TYPES 2026
Skyline of Lindholmen where TYPES 2026 was held. [Zoom in! 🔍 ]
Skyline of Lindholmen where TYPES 2026 was held. [Zoom in! 🔍 ]

This week was TYPES 2026. As usual, TYPES was a nice conference, with lots of likeminded people gathered to discuss type theory. I thought the talks this year held a good level, especially the invited talks. And I got to exchange ideas with new and old friends in the community. Zhili presented our joint work on higher kinded containers.

I stayed in a hotel next to Karlatornet, which is the phallic tower you see above. I quite enjoyed Gothenburg this time around, but did not do much sight-seeing, except for dining excursions and a visit to Backa Boulder. This year’s conference I felt was better paced than previous years, where I have felt that there have been just too many talks, and too busy programme.

Flying back to Bergen tonight.

/diary/2026-05.html#2026-05-08
2026-05-02, Friday
Show full content
Light & Shadows

There is something I haven’t mentioned here. But it is something I have poured a lot of my spare time into the last year. There will be a series on this website about it, someday… But for now, I will just leave this video here.

There are still artifacts, still not super smooth. Still temp assets. But there is light, there are shadows, and it was written in Haskell (and GLSL), and there are no polygon meshes at runtime.

/diary/2026-05.html#2026-05-02
2026-05-02, Friday
Show full content
Light & Shadows

There is something I haven’t mentioned here. But it is something I have poured a lot of my spare time into the last year. There will be a series on this website about it, someday… But for now, I will just leave this video here.

There are still artifacts, still not super smooth. Still temp assets. But there is light, there are shadows, and it was written in Haskell (and GLSL), and there are no polygon meshes at runtime.

/diary/2026-05.html#2026-05-02
2026-04-24, Friday
Show full content
Firefox styling

The modern-looking Firefox does not arouse joy in my heart. So, I decided to apply a bit of styling to it, using userChrome.css and Firefox Color. The userChrome.css I set globally for all my machines via Home Manager, while I have been picking the colours individually for all machines, to match their individual colour themes. On my laptop, I went with a beige variant:

Firefox on my laptop. [Zoom in 🔍]
Firefox on my laptop. [Zoom in 🔍]

As you can see, this screenshot was taken while I was looking into what has been done about programming quantum computers using functional programming languages. The left hand side of the window is occupied by Tree Style Tab – one of my absolute favourite Firefox extensions. The font is EB Garamond Small Caps. One thing to note though, Tree Style Tab is not affected by userChrome.css directly, but has its own CSS styling in the advanced settings.

/diary/2026-04.html#2026-04-24
2026-04-24, Friday
Show full content
Firefox styling

The modern-looking Firefox does not arouse joy in my heart. So, I decided to apply a bit of styling to it, using userChrome.css and Firefox Color. The userChrome.css I set globally for all my machines via Home Manager, while I have been picking the colours individually for all machines, to match their individual colour themes. On my laptop, I went with a beige variant:

Firefox on my laptop. [Zoom in 🔍]
Firefox on my laptop. [Zoom in 🔍]

As you can see, this screenshot was taken while I was looking into what has been done about programming quantum computers using functional programming languages. The left hand side of the window is occupied by Tree Style Tab – one of my absolute favourite Firefox extensions. The font is EB Garamond Small Caps. One thing to note though, Tree Style Tab is not affected by userChrome.css directly, but has its own CSS styling in the advanced settings.

/diary/2026-04.html#2026-04-24
2026-04-23, Thursday
Show full content
Crows

Crows might be my favourite bird. They look cool, they are smart and they are much more polite than, say, pigeons or seagulls. Having noticed that they all disappear from my neighbourhood at dusk, I found out that they do communal roosting at night. Isn’t that something?

Crow on top of Løvstakken
Crow on top of Løvstakken
/diary/2026-04.html#2026-04-23
2026-04-23, Thursday
Show full content
Crows

Crows might be my favourite bird. They look cool, they are smart and they are much more polite than, say, pigeons or seagulls. Having noticed that they all disappear from my neighbourhood at dusk, I found out that they do communal roosting at night. Isn’t that something?

Crow on top of Løvstakken
Crow on top of Løvstakken
/diary/2026-04.html#2026-04-23
2026-04-22, Wednesday
Show full content

NixOS has become my main operating system as of late. I tried Nix, the package manager, a long time ago and liked the concept! However, I was reminded about it existence a couple of years ago, and since then I have gradually ported my machines to NixOS, one by one. Currently, only the server you are receiving this website from remains on OpenBSD. I might migrate it too, but that would be a bigger project, as it is a machine I share with other family members, and OpenBSD is just such a great server OS!

NixOS
NixOS

The main thing which draws me to NixOS is the reproducibility and automation. I flake all my projects these days. That way my dependencies stay put, and I easily get a consistent development experience no matter which machine I sit down to code on.

Home Manager is another draw. I used to have a repo with all my config file and then manually symlink the files into the right location to update them between machines. This worked very well, but was a hassle to set up everytime I installed a new machine. Home Manager is a systematic solution where you write your config in Nix and it builds the config files and places them in the correct location! Many many programs have built in support, and if the particular program you want to configure does not have built-in support you can write your own, or just specify the config verbatim.

I had a bit of an adventure installing NixOS my work laptop durign Easter. I had not brought any USB stick to the cabin, so I was forced to look for an unconventional solution. I quickly disregarded nixos-infect because that shit should be illegal (I mean that in the most complementary sense!). On the other hand the kexec seemed more geared towards installing from a different machine. So I went the manual route of loopbacking the normal installation ISO image from Grub:

menuentry "NixOS Graphical Installer" {
    iso_path="/nixos-graphical-25.11.8478.bcd464ccd2a1-x86_64-linux.iso"
    export iso_path
    insmod lvm
    set root=(lvm/system-scratch)
    loopback loop $iso_path
    root=(loop)
    configfile /boot/grub/loopback.cfg
    loopback --delete loop
}

It was a bit fiddly, but I got it working! I even remembered to copy the image to RAM upon boot, so that it did not self-destruct during the installation ☺

/diary/2026-04.html#2026-04-22
2026-04-22, Wednesday
Show full content

NixOS has become my main operating system as of late. I tried Nix, the package manager, a long time ago and liked the concept! However, I was reminded about it existence a couple of years ago, and since then I have gradually ported my machines to NixOS, one by one. Currently, only the server you are receiving this website from remains on OpenBSD. I might migrate it too, but that would be a bigger project, as it is a machine I share with other family members, and OpenBSD is just such a great server OS!

NixOS
NixOS

The main thing which draws me to NixOS is the reproducibility and automation. I flake all my projects these days. That way my dependencies stay put, and I easily get a consistent development experience no matter which machine I sit down to code on.

Home Manager is another draw. I used to have a repo with all my config file and then manually symlink the files into the right location to update them between machines. This worked very well, but was a hassle to set up everytime I installed a new machine. Home Manager is a systematic solution where you write your config in Nix and it builds the config files and places them in the correct location! Many many programs have built in support, and if the particular program you want to configure does not have built-in support you can write your own, or just specify the config verbatim.

I had a bit of an adventure installing NixOS my work laptop durign Easter. I had not brought any USB stick to the cabin, so I was forced to look for an unconventional solution. I quickly disregarded nixos-infect because that shit should be illegal (I mean that in the most complementary sense!). On the other hand the kexec seemed more geared towards installing from a different machine. So I went the manual route of loopbacking the normal installation ISO image from Grub:

menuentry "NixOS Graphical Installer" {
    iso_path="/nixos-graphical-25.11.8478.bcd464ccd2a1-x86_64-linux.iso"
    export iso_path
    insmod lvm
    set root=(lvm/system-scratch)
    loopback loop $iso_path
    root=(loop)
    configfile /boot/grub/loopback.cfg
    loopback --delete loop
}

It was a bit fiddly, but I got it working! I even remembered to copy the image to RAM upon boot, so that it did not self-destruct during the installation ☺

/diary/2026-04.html#2026-04-22
2026-03-07, Saturday
Show full content

Thinking hard about capability based security these days. More on this later.

/diary/2026-03.html#2026-03-07
2026-03-07, Saturday
Show full content

Thinking hard about capability based security these days. More on this later.

/diary/2026-03.html#2026-03-07
2026-02-08, Sunday
Show full content
Late night synthing

Been a while since I played on my synth. But it never disappoints. I play for myself, and I can just lose myself in the sounds. This time I ended up just playing into an effect module, and enjoying the fruits of feedback:

Late night synth

This is of course not a “real” track, just a bit of (unlistenable) improvisation. But, I really enjoyed the detuning of the delay effect.

/diary/2026-02.html#2026-02-08
2026-02-08, Sunday
Show full content
Late night synthing

Been a while since I played on my synth. But it never disappoints. I play for myself, and I can just lose myself in the sounds. This time I ended up just playing into an effect module, and enjoying the fruits of feedback:

Late night synth

This is of course not a “real” track, just a bit of (unlistenable) improvisation. But, I really enjoyed the detuning of the delay effect.

/diary/2026-02.html#2026-02-08
2026-02-01, Sunday
Show full content
Tenure track: [██████████] 100% complete!

As of today, I am a professor at the University of Bergen.

The sign on my office door! (Still feel like it says “404 – Håkon not found”) Zoom in 🔍
The sign on my office door! (Still feel like it says “404 – Håkon not found”) Zoom in 🔍
/diary/2026-02.html#2026-02-01
2026-02-01, Sunday
Show full content
Tenure track: [██████████] 100% complete!

As of today, I am a professor at the University of Bergen.

The sign on my office door! (Still feel like it says “404 – Håkon not found”) Zoom in 🔍
The sign on my office door! (Still feel like it says “404 – Håkon not found”) Zoom in 🔍
/diary/2026-02.html#2026-02-01
2026-01-30, Friday
Show full content

We are now a couple of weeks into the functional programming course, and thus far we have covered untyped λ-calculus, simply typed λ-calculus and algebraic types, functors and today we started on monads. The course is fast paced, and we have some of the lectures at 8AM, which the students and I both find a bit early. But for those early lectures I bring a water boiler, Yorkshire tea, and crackers for everyone!

/diary/2026-01.html#2026-01-30
2026-01-30, Friday
Show full content

We are now a couple of weeks into the functional programming course, and thus far we have covered untyped λ-calculus, simply typed λ-calculus and algebraic types, functors and today we started on monads. The course is fast paced, and we have some of the lectures at 8AM, which the students and I both find a bit early. But for those early lectures I bring a water boiler, Yorkshire tea, and crackers for everyone!

/diary/2026-01.html#2026-01-30
2026-01-11, Sunday
Show full content
Lecturing Advanced Functional Programming, again!

It is time for another round of my course INF221, “Advanced Functional Programming”. The course has a lot of great topics, like Software Transactional Memory, monad transformers, dependent types and algebaric effects. Hope we have an interested crew of students this year!

First lecture is tomorrow, and I am wondering how I will do my lecturing. I hate the laptop the university provides for me, but I am unsure if my HDMI converter for my iPhone play’s ball with the projector in the assigned room. I love lecturing from the phone though.

Totally not creepy poster for the course! This characteristic, uncanny valley, weird shit is one of few redeeming quality of AI “art”.
Totally not creepy poster for the course! This characteristic, uncanny valley, weird shit is one of few redeeming quality of AI “art”.
Water, get back!

No water this week. Bergen is usually not a cold place – it is mostly just wet and chilly. Even in winter the temperature rarely stays below 0°C for long. But the last week and a half we have been in the two-digit minus, and the water in our apartment completely froze while we were in the cabin. I think the pipes are fairly new, and they put too little insulation on them when they installed them. Because they froze last year as well.

In the weekend it thawed a bit outside, and tonight we have water flowing again. Looking forward to get some clothes washed and being able to use the dishwasher!

/diary/2026-01.html#2026-01-11
2026-01-11, Sunday
Show full content
Lecturing Advanced Functional Programming, again!

It is time for another round of my course INF221, “Advanced Functional Programming”. The course has a lot of great topics, like Software Transactional Memory, monad transformers, dependent types and algebaric effects. Hope we have an interested crew of students this year!

First lecture is tomorrow, and I am wondering how I will do my lecturing. I hate the laptop the university provides for me, but I am unsure if my HDMI converter for my iPhone play’s ball with the projector in the assigned room. I love lecturing from the phone though.

Totally not creepy poster for the course! This characteristic, uncanny valley, weird shit is one of few redeeming quality of AI “art”.
Totally not creepy poster for the course! This characteristic, uncanny valley, weird shit is one of few redeeming quality of AI “art”.
Water, get back!

No water this week. Bergen is usually not a cold place – it is mostly just wet and chilly. Even in winter the temperature rarely stays below 0°C for long. But the last week and a half we have been in the two-digit minus, and the water in our apartment completely froze while we were in the cabin. I think the pipes are fairly new, and they put too little insulation on them when they installed them. Because they froze last year as well.

In the weekend it thawed a bit outside, and tonight we have water flowing again. Looking forward to get some clothes washed and being able to use the dishwasher!

/diary/2026-01.html#2026-01-11
2026-01-04, Sunday
Show full content

Last day at the cabin, before heading back home.

Atom feed!

Yesterday I spent some time getting an atom feed for this diary. I had been deliberating for a long time how to do this, since the entries are simply headers in the Markdown files. But I decided the easiet would be to create a custom Pandoc Writer. The site’s HTML is already generated using Pandoc, and so no additional tooling was needed. Just a Lua-script and a new mkfile target. Since the Atom generator was not an indepent package, I could have a very bespoke script, without worrying of making it work for any other purpose than my own. The only feature I added was an attribute for excluding entries from syndication:

## 2026-01-04, Sunday {#2026-01-04 syndicated=false}

This entry would not appear in the feed.

There is something to be said of bespoke systems. We all love abstraction, and general solutions. But the power of programming is that one can make tailored solutions. We need the general tools, but we should also make the general tools programmable, so that we can extend them and adapt them to our purpose. Pandoc is such a great general tool. With filters and custom readers and writers is is perfect for systems that grow.

I am very happy about the result. I will also create an atom feed for the rest of the pages on the site. But in that feed the default would be for them to be unsyndicated, and syndicated=true in the metadata header would publish them.

Git and large binaries

Another quality of life thing I did was to remove all large binary files from the website repository. This used to waste around 15GB in every working copy of the site. There is now a git ignored media/ directory in my workdir, which has the same tree structure as site-src/, but which is synced to a separate central server location using rsync. The synchronisation is hooked to git push and a commited manifest of hashes connects commits to the state of the media files, ensuring that I can deploy from any workstation without accedentally publishing the wrong version of a binary file. So, any time I do mk deploy the currently commited manifest is verified against the files pushed.

To test the website locally, there is a staging area, where I link in the media files mentioned in the deployment index. Thus, I get an accurate testing server on the workstation, before doing any actual deployment.

All in all, I hope the improvement made over the holidays should make working on the site a much smoother experience.

/diary/2026-01.html#2026-01-04
2026-01-04, Sunday
Show full content

Last day at the cabin, before heading back home.

Atom feed!

Yesterday I spent some time getting an atom feed for this diary. I had been deliberating for a long time how to do this, since the entries are simply headers in the Markdown files. But I decided the easiet would be to create a custom Pandoc Writer. The site’s HTML is already generated using Pandoc, and so no additional tooling was needed. Just a Lua-script and a new mkfile target. Since the Atom generator was not an indepent package, I could have a very bespoke script, without worrying of making it work for any other purpose than my own. The only feature I added was an attribute for excluding entries from syndication:

## 2026-01-04, Sunday {#2026-01-04 syndicated=false}

This entry would not appear in the feed.

There is something to be said of bespoke systems. We all love abstraction, and general solutions. But the power of programming is that one can make tailored solutions. We need the general tools, but we should also make the general tools programmable, so that we can extend them and adapt them to our purpose. Pandoc is such a great general tool. With filters and custom readers and writers is is perfect for systems that grow.

I am very happy about the result. I will also create an atom feed for the rest of the pages on the site. But in that feed the default would be for them to be unsyndicated, and syndicated=true in the metadata header would publish them.

Git and large binaries

Another quality of life thing I did was to remove all large binary files from the website repository. This used to waste around 15GB in every working copy of the site. There is now a git ignored media/ directory in my workdir, which has the same tree structure as site-src/, but which is synced to a separate central server location using rsync. The synchronisation is hooked to git push and a commited manifest of hashes connects commits to the state of the media files, ensuring that I can deploy from any workstation without accedentally publishing the wrong version of a binary file. So, any time I do mk deploy the currently commited manifest is verified against the files pushed.

To test the website locally, there is a staging area, where I link in the media files mentioned in the deployment index. Thus, I get an accurate testing server on the workstation, before doing any actual deployment.

All in all, I hope the improvement made over the holidays should make working on the site a much smoother experience.

/diary/2026-01.html#2026-01-04
2026-01-02, Friday
Show full content

Wonderful times here at the cabin. Snow and good weather. I also brought my computer so that I can work a bit. Yesterday I nixed the development environment for my website, and reworked the mkfile which builds and deploys it. I also separated out the media files out of the git repo, so that they are no longer kept in it.

The mountain is beautiful! [Zoom in 🔍]
The mountain is beautiful! [Zoom in 🔍]
/diary/2026-01.html#2026-01-02
2026-01-02, Friday
Show full content

Wonderful times here at the cabin. Snow and good weather. I also brought my computer so that I can work a bit. Yesterday I nixed the development environment for my website, and reworked the mkfile which builds and deploys it. I also separated out the media files out of the git repo, so that they are no longer kept in it.

The mountain is beautiful! [Zoom in 🔍]
The mountain is beautiful! [Zoom in 🔍]
/diary/2026-01.html#2026-01-02
2026-01-01, Thursday
Show full content
New Year

Celebrating New Year at the cabin! Looking forward to the new year, hoping it will be a good one!

Fireworks long since lost their magic for me, even though I still walk outside to view them at the midnight stroke. It just seems like one of these things which do not actually make sense once you think about it. Yes, pretty colours and bangs are nice, but no doubt tomorrow we shall read about all the eye injuries, the fires started, and the scared to death animals.

Quite a lot fireworks around the cabin this year. [Zoom in 🔍]
Quite a lot fireworks around the cabin this year. [Zoom in 🔍]
/diary/2026-01.html#2026-01-01
2026-01-01, Thursday
Show full content
New Year

Celebrating New Year at the cabin! Looking forward to the new year, hoping it will be a good one!

Fireworks long since lost their magic for me, even though I still walk outside to view them at the midnight stroke. It just seems like one of these things which do not actually make sense once you think about it. Yes, pretty colours and bangs are nice, but no doubt tomorrow we shall read about all the eye injuries, the fires started, and the scared to death animals.

Quite a lot fireworks around the cabin this year. [Zoom in 🔍]
Quite a lot fireworks around the cabin this year. [Zoom in 🔍]
/diary/2026-01.html#2026-01-01
2025-10-30, Thursday
Show full content

Found some old sketches I made many years ago in The Stockholm Logic Seminar. At that time, the seminar was held in room 16 of building 5 at Kräftriket. Peter LeFanu Lumsdaine held the seminar, but I not sure exact which one this was, maybe 2015 or 2016. Judging by the blackboard content it had something to do with the semantics of type theory. I was paying attention to the talk, but also just doodling away on my note book. The result was a set of small sketches of the people listening, as well as the speaker himself.

My original sketches were crude, so I will not be uploading those, but I gave them to an LLM and asked it to clean them up slightly. I felt they somewhat captured the characters in the room. I miss those days, and I miss Erik in particular. My time as a PhD student at Stockholm University was a good one!

Peter LeFanu Lumsdaine giving a talk at The Stockholm Logic Seminar [Zoom in 🔍]
Peter LeFanu Lumsdaine giving a talk at The Stockholm Logic Seminar [Zoom in 🔍]
Per Martin-Löf listening attentively. He always ask insightful questions during talks. [Zoom in 🔍]
Per Martin-Löf listening attentively. He always ask insightful questions during talks. [Zoom in 🔍]
Erik Palmgren organised the seminar in those days. [Zoom in 🔍]
Erik Palmgren organised the seminar in those days. [Zoom in 🔍]
Jacopo Emmenegger was a PhD student in Stockholm at the same time as me. [Zoom in 🔍]
Jacopo Emmenegger was a PhD student in Stockholm at the same time as me. [Zoom in 🔍]
/diary/2025-10.html#2025-10-30
2025-10-30, Thursday
Show full content

Found some old sketches I made many years ago in The Stockholm Logic Seminar. At that time, the seminar was held in room 16 of building 5 at Kräftriket. Peter LeFanu Lumsdaine held the seminar, but I not sure exact which one this was, maybe 2015 or 2016. Judging by the blackboard content it had something to do with the semantics of type theory. I was paying attention to the talk, but also just doodling away on my note book. The result was a set of small sketches of the people listening, as well as the speaker himself.

My original sketches were crude, so I will not be uploading those, but I gave them to an LLM and asked it to clean them up slightly. I felt they somewhat captured the characters in the room. I miss those days, and I miss Erik in particular. My time as a PhD student at Stockholm University was a good one!

Peter LeFanu Lumsdaine giving a talk at The Stockholm Logic Seminar [Zoom in 🔍]
Peter LeFanu Lumsdaine giving a talk at The Stockholm Logic Seminar [Zoom in 🔍]
Per Martin-Löf listening attentively. He always ask insightful questions during talks. [Zoom in 🔍]
Per Martin-Löf listening attentively. He always ask insightful questions during talks. [Zoom in 🔍]
Erik Palmgren organised the seminar in those days. [Zoom in 🔍]
Erik Palmgren organised the seminar in those days. [Zoom in 🔍]
Jacopo Emmenegger was a PhD student in Stockholm at the same time as me. [Zoom in 🔍]
Jacopo Emmenegger was a PhD student in Stockholm at the same time as me. [Zoom in 🔍]
/diary/2025-10.html#2025-10-30
2025-07-09, Wednesday
Show full content

Elisabeth and I went hiking in Kvanndalen. The terrain was slightly more challenging than we expected, but the reward was stunning views and beautiful surroundings. At times we really had to cling to the sides of valley above steep gorges. We camped roughly in the middle of the valley, just slightly further down than the farthest one can see on the picture below. We originally planned hiking around and back to Haukelisæter again, but our slow progress the first day meant we opted to walk down to Bleskestad, just above Roalkvam, and get my father to pick us up.

Kvanndalen. [Zoom in 🔍]
Kvanndalen. [Zoom in 🔍]
/diary/2025-07.html#2025-07-09
2025-07-09, Wednesday
Show full content

Elisabeth and I went hiking in Kvanndalen. The terrain was slightly more challenging than we expected, but the reward was stunning views and beautiful surroundings. At times we really had to cling to the sides of valley above steep gorges. We camped roughly in the middle of the valley, just slightly further down than the farthest one can see on the picture below. We originally planned hiking around and back to Haukelisæter again, but our slow progress the first day meant we opted to walk down to Bleskestad, just above Roalkvam, and get my father to pick us up.

Kvanndalen. [Zoom in 🔍]
Kvanndalen. [Zoom in 🔍]
/diary/2025-07.html#2025-07-09
2024-10-25, Friday
Show full content

Spending the (long) weekend in Vågsli at my parents cabin. Perhaps the last weekend before the snow. I was here a couple of weeks ago, and then it was snowing. But the snow melted again.

/diary/2024-10.html#2024-10-25
2024-10-25, Friday
Show full content

Spending the (long) weekend in Vågsli at my parents cabin. Perhaps the last weekend before the snow. I was here a couple of weeks ago, and then it was snowing. But the snow melted again.

/diary/2024-10.html#2024-10-25
2024-05-24, Friday
Show full content

Over the winter, I have been refining a Haskell library of functions for doing Applicative Logic. The idea is that a lot of functions involving booleans can be generalised to work on any Applicative Functor (possibly applied to Monoids), through the isomorphism Bool ≃ Maybe () – where Maybe is the applicative functor and () is the monad.

There is a more complete write-up here on my website, and I have put the library on Hackage. There is also a discussion thread on r/haskell under the heading “A boolean is maybe true”. I was happy that some people got the point, and there was even a link to my write-up in Haskell Weekly.

/diary/2024-05.html#2024-05-24
2024-05-24, Friday
Show full content

Over the winter, I have been refining a Haskell library of functions for doing Applicative Logic. The idea is that a lot of functions involving booleans can be generalised to work on any Applicative Functor (possibly applied to Monoids), through the isomorphism Bool ≃ Maybe () – where Maybe is the applicative functor and () is the monad.

There is a more complete write-up here on my website, and I have put the library on Hackage. There is also a discussion thread on r/haskell under the heading “A boolean is maybe true”. I was happy that some people got the point, and there was even a link to my write-up in Haskell Weekly.

/diary/2024-05.html#2024-05-24
2024-04-04, Thursday
Show full content

Been to HoTT-UF 2024 in Leuven, Belgium. Which was really nice! Both Thorsten Altenkirch and his PhD student, Stefania Damato, were giving container-themed talks, which has rejuvenated my interest in containers. Thorsten and I discussed higher-order containers after his talk, and we both had ideas for how to it.

Approaching Brussels. [Zoom in 🔍]
Approaching Brussels. [Zoom in 🔍]
/diary/2024-04.html#2024-04-04
2024-04-04, Thursday
Show full content

Been to HoTT-UF 2024 in Leuven, Belgium. Which was really nice! Both Thorsten Altenkirch and his PhD student, Stefania Damato, were giving container-themed talks, which has rejuvenated my interest in containers. Thorsten and I discussed higher-order containers after his talk, and we both had ideas for how to it.

Approaching Brussels. [Zoom in 🔍]
Approaching Brussels. [Zoom in 🔍]
/diary/2024-04.html#2024-04-04
2023-01-25, Wednesday
Show full content

So, tonight I found myself trying in vain to start the car, with the boot full of shit. Literally, shit. I was on my way to empty the aforementioned Porta Potty and apparently the battery was flat.

Luckily, the place to empty is just a 15-minute stroll from here! [Zoom in 🔍]
Luckily, the place to empty is just a 15-minute stroll from here! [Zoom in 🔍]
/diary/2023-01.html#2023-01-25
2023-01-25, Wednesday
Show full content

So, tonight I found myself trying in vain to start the car, with the boot full of shit. Literally, shit. I was on my way to empty the aforementioned Porta Potty and apparently the battery was flat.

Luckily, the place to empty is just a 15-minute stroll from here! [Zoom in 🔍]
Luckily, the place to empty is just a 15-minute stroll from here! [Zoom in 🔍]
/diary/2023-01.html#2023-01-25
2023-01-20, Friday
Show full content

Today was the first lecture of my new course, INF221: Advanced Functional Programming. The little room which had been assigned to us was packed, but hopefully we will get a bigger room.

/diary/2023-01.html#2023-01-20
2023-01-20, Friday
Show full content

Today was the first lecture of my new course, INF221: Advanced Functional Programming. The little room which had been assigned to us was packed, but hopefully we will get a bigger room.

/diary/2023-01.html#2023-01-20
2023-01-02, Monday
Show full content

Today our long awaited bathroom renovation starts. In a few days time we will have to do our business out on the balcony in a Porta Potty. At least we will have a view towards Ulriken as we take a shit.

/diary/2023-01.html#2023-01-02
2023-01-02, Monday
Show full content

Today our long awaited bathroom renovation starts. In a few days time we will have to do our business out on the balcony in a Porta Potty. At least we will have a view towards Ulriken as we take a shit.

/diary/2023-01.html#2023-01-02
2022-12-23, Friday
Show full content

Lille-julaften (“Little Christmas Eve”) here in Norway. As usual, I am visiting my parents over the holiday, along with the rest of the family. This year’s new arrival, my sister’s daughter, is getting to know her cousins. In the evening we played the Dune boardgame, which is so much fun! Especially the battles are nerve-wrecking!

The spice must flow on Arrakis! But so too must the caffeinated drinks, keeping us sharp in intrigues that last into the wee hours. [Zoom in 🔍]
The spice must flow on Arrakis! But so too must the caffeinated drinks, keeping us sharp in intrigues that last into the wee hours. [Zoom in 🔍]
/diary/2022-12.html#2022-12-23
2022-12-23, Friday
Show full content

Lille-julaften (“Little Christmas Eve”) here in Norway. As usual, I am visiting my parents over the holiday, along with the rest of the family. This year’s new arrival, my sister’s daughter, is getting to know her cousins. In the evening we played the Dune boardgame, which is so much fun! Especially the battles are nerve-wrecking!

The spice must flow on Arrakis! But so too must the caffeinated drinks, keeping us sharp in intrigues that last into the wee hours. [Zoom in 🔍]
The spice must flow on Arrakis! But so too must the caffeinated drinks, keeping us sharp in intrigues that last into the wee hours. [Zoom in 🔍]
/diary/2022-12.html#2022-12-23
2022-11-11, Friday
Show full content

Had an evening by myself. Spent most of it deep into my synth, exploring sounds and melodies. At some point I felt like I was having a party:

The sound is sub par since I was just recording it through my iPhone 7. And I made no recordings, but sometimes the point is just to play for my own enjoyment.

/diary/2022-11.html#2022-11-11
2022-11-11, Friday
Show full content

Had an evening by myself. Spent most of it deep into my synth, exploring sounds and melodies. At some point I felt like I was having a party:

The sound is sub par since I was just recording it through my iPhone 7. And I made no recordings, but sometimes the point is just to play for my own enjoyment.

/diary/2022-11.html#2022-11-11
2022-10-30, Sunday
Show full content

Starting to see the end of the term approaching. Less than a month until my students have their final exam. For me “to see a date approaching” is quite literal. I see dates very clearly in my mind. They are distributed counter-clockwise on a roundish landscape which represents the year. As the year progresses my vantage point in this landscape moves so that I always see things from today’s date. Thus, the coming dates are approaching. There is also a kind of covering-space effect where the actual dates over many years cover the same landscape. In a path-lifting kind of way, I can see forward into the future, say next march, or backwards to the past, say to the previous march.

Next week we have a conference, Nordic Workshop on Programming Theory, which I am on the organisation committee1 for.


  1. I love the amount of double letters in the word “committee”.↩︎

/diary/2022-10.html#2022-10-30
2022-10-30, Sunday
Show full content

Starting to see the end of the term approaching. Less than a month until my students have their final exam. For me “to see a date approaching” is quite literal. I see dates very clearly in my mind. They are distributed counter-clockwise on a roundish landscape which represents the year. As the year progresses my vantage point in this landscape moves so that I always see things from today’s date. Thus, the coming dates are approaching. There is also a kind of covering-space effect where the actual dates over many years cover the same landscape. In a path-lifting kind of way, I can see forward into the future, say next march, or backwards to the past, say to the previous march.

Next week we have a conference, Nordic Workshop on Programming Theory, which I am on the organisation committee1 for.


  1. I love the amount of double letters in the word “committee”.↩︎

/diary/2022-10.html#2022-10-30
2022-09-30, Friday
Show full content

Went bouldering after work with a group of co-workers. It’s been a busy week, so it was good to just go do something physical. Climbing is a good way to exercise because it is just fun enough that you don’t notice that you are exercising. Each bouldering route is like a puzzle. Of course there is skill and physical form involved, but your thinking-brain is also involved. You need to figure out how to position your various limbs and move them in order for the route to be possible

«Climber», medium: MidJourney [Zoom in 🔍]
«Climber», medium: MidJourney [Zoom in 🔍]

I am starting to get the hang of MidJourney now. And it is exciting! I like discovering what my prompts turn into. I don’t know anything about Brownsville, but I like the result which the word “Brownsville” prompted below!

«Dancing on the streets of Brownsville», medium: MidJourney [Zoom in 🔍]
«Dancing on the streets of Brownsville», medium: MidJourney [Zoom in 🔍]
/diary/2022-09.html#2022-09-30
2022-09-30, Friday
Show full content

Went bouldering after work with a group of co-workers. It’s been a busy week, so it was good to just go do something physical. Climbing is a good way to exercise because it is just fun enough that you don’t notice that you are exercising. Each bouldering route is like a puzzle. Of course there is skill and physical form involved, but your thinking-brain is also involved. You need to figure out how to position your various limbs and move them in order for the route to be possible

«Climber», medium: MidJourney [Zoom in 🔍]
«Climber», medium: MidJourney [Zoom in 🔍]

I am starting to get the hang of MidJourney now. And it is exciting! I like discovering what my prompts turn into. I don’t know anything about Brownsville, but I like the result which the word “Brownsville” prompted below!

«Dancing on the streets of Brownsville», medium: MidJourney [Zoom in 🔍]
«Dancing on the streets of Brownsville», medium: MidJourney [Zoom in 🔍]
/diary/2022-09.html#2022-09-30
2022-08-10, Wednesday
Show full content

Back at work for almost two weeks already. Mostly preparing for teaching functional programming.

Generative art

I have discovered MidJourney, one of these machine learning image generation tools where you write a prompt and it generates an image. It is really fun! Of course it has its strengths and weaknesses. But, more than with other “AI things”, I feel like this has real, human value. Also, the community around MidJourney is exciting.

A mindflayer, adapted to a D&D champaign set in a fantasy dessert world. [Zoom in 🔍]
A mindflayer, adapted to a D&D champaign set in a fantasy dessert world. [Zoom in 🔍]

Generative art is nothing new. The core of generative art is that you write an algorithm which generates the art, rather than “performing it” yourself. Often you incorporate some source of randomness into the process, so that you can get a number of variations on the same theme. The algorithm can also take some user input, which affects the result in some way.

In the case where you wrote the algorithm, the result is clearly art you have made. But even if you are merely using someone else’s algorithm, you might claim that the result is art you have made, if one or a combination of the follow two cases hold:

  1. Your input to the algorithm enabled your artistic expression.
  2. Your selection of this output from many randomly generated outputs enabled your artistic expression.
Musical example

Here is a simple example from music of the second case: In modular synthesis you make music by connecting modules together to form a synthesiser.

Often the notes played is determined by a sequencer module, instead of using a keyboard. Some sequencers allow you to program in a sequence of notes played manually, but there is a sequencer called “Turing Machine”1 which generates random sequences of notes.

The crucial thing about the Turing Machine is that it will play random notes until you lock it. Once the sequence is locked it will keep playing the last generated sequence until you unlock it. So, to produce a cool bassline for your track, you connect the Turing machine to the bass modules, and listen to its random playing until you find something you like. Then you lock it in, and that’s it! Clearly it is your bassline because you chose it among all the ones generated by the Turing Machine.

Here is a track where Mutable Instruments’ Marbles, another module like the Turing Machine2, is used to decide the melody played:

Foot Stomp

The theme you hear repeat a few times throughout track was chosen by just letting Marbles “roll the dice” until a catchy melody came out. Then I was free to focus on other parts, such was how to make the most bad-ass distorted sound to play that melody with.

BTW, that distorted sound is a harmonic oscillator (sum of related sine waves) modulating a through-zero FM oscillator. Controlling the distribution of sines gives absolutely interesting shifts in timbre!

DALL-E, MidJourney and others

Currently, there are several competing prompted-image-generators. But the idea is that you give a short prompt such as “The invention of pizza by god, Italian renaissance painting”, and the program spits out:

A critical moment in time, forever captured by this renaissance painting. [Zoom in 🔍]
A critical moment in time, forever captured by this renaissance painting. [Zoom in 🔍]

In MidJourney the output is actually four images, and then you can iterate, making variations on each of them. This means that both the first and the second point above apply. The user provides both input to the algorithm, and selects from a supply of randomly generated output.

In both ways this enables the user to express themselves artistically. And this is the value I see in this: it enables more people to express themselves creatively using computer graphics. For instance, I will use MidJourney when creating concept art for my D&D sessions. The dessert mind flayer above is way better drawn that I would have been able to if I sat down in Krita or Blender.

Now, I don’t think MidJourney or DALL-E are any threat to actually skilled artists. A human artist actually understands what they are drawing, and can be relied upon in a completely different way. The pictures generated by MidJourney usually have very recognizable artefacts. And most importantly, the control you have when generating the picture is very tenuous. You might have a perfect idea in your head, but the algorithm is not a mind reader, so the picture coming out is usually completely different. Sometimes that’s OK, and a cool feature. But for most of the kind of work you pay an artist for, it would be completely useless.

Also, artists often produce 3D models, which can be rendered in different settings and reposed. This has very high utility compared to the lump of pixels from MidJourney.


  1. No relation to the mathematical model of computation, except for the name.↩︎

  2. Marbles has the advantage of being able to do non-destructive variations, where you randomize the notes for a time then return to the previously locked tune.↩︎

/diary/2022-08.html#2022-08-10
2022-08-10, Wednesday
Show full content

Back at work for almost two weeks already. Mostly preparing for teaching functional programming.

Generative art

I have discovered MidJourney, one of these machine learning image generation tools where you write a prompt and it generates an image. It is really fun! Of course it has its strengths and weaknesses. But, more than with other “AI things”, I feel like this has real, human value. Also, the community around MidJourney is exciting.

A mindflayer, adapted to a D&D champaign set in a fantasy dessert world. [Zoom in 🔍]
A mindflayer, adapted to a D&D champaign set in a fantasy dessert world. [Zoom in 🔍]

Generative art is nothing new. The core of generative art is that you write an algorithm which generates the art, rather than “performing it” yourself. Often you incorporate some source of randomness into the process, so that you can get a number of variations on the same theme. The algorithm can also take some user input, which affects the result in some way.

In the case where you wrote the algorithm, the result is clearly art you have made. But even if you are merely using someone else’s algorithm, you might claim that the result is art you have made, if one or a combination of the follow two cases hold:

  1. Your input to the algorithm enabled your artistic expression.
  2. Your selection of this output from many randomly generated outputs enabled your artistic expression.
Musical example

Here is a simple example from music of the second case: In modular synthesis you make music by connecting modules together to form a synthesiser.

Often the notes played is determined by a sequencer module, instead of using a keyboard. Some sequencers allow you to program in a sequence of notes played manually, but there is a sequencer called “Turing Machine”1 which generates random sequences of notes.

The crucial thing about the Turing Machine is that it will play random notes until you lock it. Once the sequence is locked it will keep playing the last generated sequence until you unlock it. So, to produce a cool bassline for your track, you connect the Turing machine to the bass modules, and listen to its random playing until you find something you like. Then you lock it in, and that’s it! Clearly it is your bassline because you chose it among all the ones generated by the Turing Machine.

Here is a track where Mutable Instruments’ Marbles, another module like the Turing Machine2, is used to decide the melody played:

Foot Stomp

The theme you hear repeat a few times throughout track was chosen by just letting Marbles “roll the dice” until a catchy melody came out. Then I was free to focus on other parts, such was how to make the most bad-ass distorted sound to play that melody with.

BTW, that distorted sound is a harmonic oscillator (sum of related sine waves) modulating a through-zero FM oscillator. Controlling the distribution of sines gives absolutely interesting shifts in timbre!

DALL-E, MidJourney and others

Currently, there are several competing prompted-image-generators. But the idea is that you give a short prompt such as “The invention of pizza by god, Italian renaissance painting”, and the program spits out:

A critical moment in time, forever captured by this renaissance painting. [Zoom in 🔍]
A critical moment in time, forever captured by this renaissance painting. [Zoom in 🔍]

In MidJourney the output is actually four images, and then you can iterate, making variations on each of them. This means that both the first and the second point above apply. The user provides both input to the algorithm, and selects from a supply of randomly generated output.

In both ways this enables the user to express themselves artistically. And this is the value I see in this: it enables more people to express themselves creatively using computer graphics. For instance, I will use MidJourney when creating concept art for my D&D sessions. The dessert mind flayer above is way better drawn that I would have been able to if I sat down in Krita or Blender.

Now, I don’t think MidJourney or DALL-E are any threat to actually skilled artists. A human artist actually understands what they are drawing, and can be relied upon in a completely different way. The pictures generated by MidJourney usually have very recognizable artefacts. And most importantly, the control you have when generating the picture is very tenuous. You might have a perfect idea in your head, but the algorithm is not a mind reader, so the picture coming out is usually completely different. Sometimes that’s OK, and a cool feature. But for most of the kind of work you pay an artist for, it would be completely useless.

Also, artists often produce 3D models, which can be rendered in different settings and reposed. This has very high utility compared to the lump of pixels from MidJourney.


  1. No relation to the mathematical model of computation, except for the name.↩︎

  2. Marbles has the advantage of being able to do non-destructive variations, where you randomize the notes for a time then return to the previously locked tune.↩︎

/diary/2022-08.html#2022-08-10
2022-07-15, Friday
Show full content
Vacation

This week we returned from a vacation trip to Stockholm. The SAS pilots are on strike, because SAS broke the contract they made to rehire pilots after the COVID-19 pandemic crisis was over. Our plane to Stockholm was scheduled 13:25, and the strike was due to start 12:00. But it turned out, that while it is a SAS route, SAS was not actually flying the plane – CityJet was. So, we got both there an back again despite the strike.

Synthy times

Today, I spent some quality time with my synth. The rack was reorganised earlier in the week and I tidied the desk it stands on. I still struggle a bit with doing several takes on multitrack recordings, but some progress is being made: A new clock divider now makes it possible to use the KeyStep 36 as a clock source. The KeyStep also starts the recording, so with a bit of practise I should be able to sync the different takes up directly.

The track I recorded today was initially by the new layout of the modules, where a choice of voices (oscillators + filter/wavefolder + envelope generator + vca) have been constructed. Aaaand, Rings is playing a baseline ☺

Looking through the memory card, I found a few other tracks which were recorded, but not edited. So, I got those done as well. I actually do very little editing after recording. All effects and mixing is done at the synth. All I really do is to even the levels a bit of different parts of the track.

Since there was a few weeks since I recorded these, I cannot really remember what inspired them. But you can listen to them here:

Actually, listening back to these, I remember that “Toy box” is in fact just the Qu-bit surface, cycling through different modes.

/diary/2022-07.html#2022-07-15
2022-07-15, Friday
Show full content
Vacation

This week we returned from a vacation trip to Stockholm. The SAS pilots are on strike, because SAS broke the contract they made to rehire pilots after the COVID-19 pandemic crisis was over. Our plane to Stockholm was scheduled 13:25, and the strike was due to start 12:00. But it turned out, that while it is a SAS route, SAS was not actually flying the plane – CityJet was. So, we got both there an back again despite the strike.

Synthy times

Today, I spent some quality time with my synth. The rack was reorganised earlier in the week and I tidied the desk it stands on. I still struggle a bit with doing several takes on multitrack recordings, but some progress is being made: A new clock divider now makes it possible to use the KeyStep 36 as a clock source. The KeyStep also starts the recording, so with a bit of practise I should be able to sync the different takes up directly.

The track I recorded today was initially by the new layout of the modules, where a choice of voices (oscillators + filter/wavefolder + envelope generator + vca) have been constructed. Aaaand, Rings is playing a baseline ☺

Looking through the memory card, I found a few other tracks which were recorded, but not edited. So, I got those done as well. I actually do very little editing after recording. All effects and mixing is done at the synth. All I really do is to even the levels a bit of different parts of the track.

Since there was a few weeks since I recorded these, I cannot really remember what inspired them. But you can listen to them here:

Actually, listening back to these, I remember that “Toy box” is in fact just the Qu-bit surface, cycling through different modes.

/diary/2022-07.html#2022-07-15
2022-06-05, Sunday
Show full content

As one might, I have been watching the fourth season of Stranger Things, and in the fourth episode there was a moment – a little joke – which I derived great pleasure from. Mostly because I imagine not a whole lot of people would notice or have the prerequisite knowledge of English garden landscaping to laugh at it.

So, for your benefit, so that you can also enjoy this little moment of the episode, let me introduce the “ha-ha”:

A comparison between ha-ha and regular walls. (842U / Wikipedia / Gnu Free Documentation Licence)
A comparison between ha-ha and regular walls. (842U / Wikipedia / Gnu Free Documentation Licence)

As you can see, a ha-ha is kind of a wall, but the ground on one side is as hight as the wall. A ha-ha is useful when you want a wall, but don’t want to ruin the view from the inside. Here is a real world example:

Hopetoun House ha-ha. (Andrew Shiva / Wikipedia / CC BY-SA 4.0)
Hopetoun House ha-ha. (Andrew Shiva / Wikipedia / CC BY-SA 4.0)

And here is one from one of my MineCraft castles:

A ha-ha keeps the monsters out of my MineCraft home
A ha-ha keeps the monsters out of my MineCraft home

Back to Stranger Things. In episode four of the forth season, Nancy and Robin visit an asylum in an attempt to get one of the inmates there to talk about how a demon killed his family fifty years ago. They pretend to be psychology students, and while they are given a tour of the place, we briefly see what looks like a ha-ha. So, like anyone with an interest in obscure walls, I nodded to myself: “Ah, see now there is a nice ha-ha, if ever I saw one.”

Nancy and Robin get to talk with the fellow, but in the end their cover is blown, and they have to make a run for it. And as they do, we get a great shot showing how ha-has are almost invisible from the top:

Do you see that there is a wall here?
Do you see that there is a wall here?

For a moment I worried that they would not notice the drop and fall. Indeed, one can imagine the origin of the term “ha-ha” to be “Ha,ha! You fell and broke your leg!”. But they actually jumped down rather gracefully:

Down the ha-ha!
Down the ha-ha!

And then, the creators had a brilliant idea, as a tip of the hat to anyone enjoying the landscaping at the asylum, one of the inmates exclaims “Ha ha ha ha ha ha!”.

“Ha ha ha ha ha ha!”
“Ha ha ha ha ha ha!”

Here is the whole sequence:

/diary/2022-06.html#2022-06-05
2022-06-05, Sunday
Show full content

As one might, I have been watching the fourth season of Stranger Things, and in the fourth episode there was a moment – a little joke – which I derived great pleasure from. Mostly because I imagine not a whole lot of people would notice or have the prerequisite knowledge of English garden landscaping to laugh at it.

So, for your benefit, so that you can also enjoy this little moment of the episode, let me introduce the “ha-ha”:

A comparison between ha-ha and regular walls. (842U / Wikipedia / Gnu Free Documentation Licence)
A comparison between ha-ha and regular walls. (842U / Wikipedia / Gnu Free Documentation Licence)

As you can see, a ha-ha is kind of a wall, but the ground on one side is as hight as the wall. A ha-ha is useful when you want a wall, but don’t want to ruin the view from the inside. Here is a real world example:

Hopetoun House ha-ha. (Andrew Shiva / Wikipedia / CC BY-SA 4.0)
Hopetoun House ha-ha. (Andrew Shiva / Wikipedia / CC BY-SA 4.0)

And here is one from one of my MineCraft castles:

A ha-ha keeps the monsters out of my MineCraft home
A ha-ha keeps the monsters out of my MineCraft home

Back to Stranger Things. In episode four of the forth season, Nancy and Robin visit an asylum in an attempt to get one of the inmates there to talk about how a demon killed his family fifty years ago. They pretend to be psychology students, and while they are given a tour of the place, we briefly see what looks like a ha-ha. So, like anyone with an interest in obscure walls, I nodded to myself: “Ah, see now there is a nice ha-ha, if ever I saw one.”

Nancy and Robin get to talk with the fellow, but in the end their cover is blown, and they have to make a run for it. And as they do, we get a great shot showing how ha-has are almost invisible from the top:

Do you see that there is a wall here?
Do you see that there is a wall here?

For a moment I worried that they would not notice the drop and fall. Indeed, one can imagine the origin of the term “ha-ha” to be “Ha,ha! You fell and broke your leg!”. But they actually jumped down rather gracefully:

Down the ha-ha!
Down the ha-ha!

And then, the creators had a brilliant idea, as a tip of the hat to anyone enjoying the landscaping at the asylum, one of the inmates exclaims “Ha ha ha ha ha ha!”.

“Ha ha ha ha ha ha!”
“Ha ha ha ha ha ha!”

Here is the whole sequence:

/diary/2022-06.html#2022-06-05
2022-05-20, Friday
Show full content

In Stockholm for a meeting in the EuroProofNet COST action’s 6th working group. Feels good to visit Kräftriket one last time before the math department there moves to new facilities across the road. Kräftriket is so beautiful in summer, and I have many fond memories from my time there. Even got to say hello again to Per Martin-Löf who is still active in attending seminars!

Group photo from the workshop
Group photo from the workshop
/diary/2022-05.html#2022-05-20
2022-05-20, Friday
Show full content

In Stockholm for a meeting in the EuroProofNet COST action’s 6th working group. Feels good to visit Kräftriket one last time before the math department there moves to new facilities across the road. Kräftriket is so beautiful in summer, and I have many fond memories from my time there. Even got to say hello again to Per Martin-Löf who is still active in attending seminars!

Group photo from the workshop
Group photo from the workshop
/diary/2022-05.html#2022-05-20