Håkon Robbestad Gylterud

This is my public diary.

2017 2018
November January
December February

2018–12–06, Thursday

Back from Oslo, where I visited CAS and gave a talk and presented the proto-type of my type theory specification library. Always pleasant to visit Oslo, which for me is full of memories — both from my time studying there, but also from when we lived there when I was a child. During my studies I had a lot of time to walk the city, and I must have walked almost every street from Bjerke to Fornebu1.

Together with writing, I find walking to be an execellent way to process complex thoughts. There are possibly several reasons for this (increased blood circulation, just the right amount of sensory stimuli, the privacy of being a stranger to everyone you meet) but I always valued most the sense of purpose which comes with a walk.

2018–12–10, Monday

Ulriken has put on a coat of snow today. Here, further down, we got rain instead. A few cups of good tea helps me throught a pile of exams in need of grading. At home I play the rôle of electrician, making light on the balcony.

2018–12–31, Monday

Celebrating new-year in Saint-Petersburg. During the day, streets were filled with smiling people – just walking about, or on their way to visit friends and family. I admit to smiling in the sunny weather as well. While the wide streets of Saint Petersburg makes it feel a bit barren and cold at times, this is quickly remidied by laughing children running around in the snow, or adults on their way with their arms full of gifts from Дед Мороз.

2019–01–10, Thursday

Autogenerating e-mail addresses on OpenBSD and OpenSMTPD

Wrote a small shell script which generates new e-mail aliases. This is useful if you do not want to trust some site with your real address. The script is quite specific to my set-up, but should be easily adaptable to other settings.

In short, you generate random aliases from the command line. For instance, to generate a new alias for use with hub.darcs.net:

user@example.com $ newmail hub.darcs.net

And if you later forgot which one you had generated:

user@example.com $ whichmail hub.darcs.net

2019–01–15, Tuesday

Listening to Fearofdark – Motorway, which Christophe2 recommended me, while formalising λ’-calculus in Agda. There are close relationships between mathematics and music, and I find that chiptunes are great while working on formalisation — but most creative part of the work requires silence for me.

2019–01–29, Wedneday

Had fun playing DnD tonight. Inspired by my recent Nethack playing I wanted some old-school monsters to appear, and landed on rustmonsters. Baern, one of the player characers, got his nice magic armor completely dissolved by rust. Old-school monsters are hard-core.

2019–02–01, Friday

Thinking quite a bit on programming language design these days. While I like pure functional programming languages, such as Haskell, I think there are improvements to be made in how they interact with the rest of the system.

As an aside, I am also experiement with practical implementations of quoting operators, based on the λ-quote calculus I have been working on lately.

2019–02–20, Wednesday

I have been doing some cosmetic changes to my website. Mostly changes in the css, but I also have been experimenting with adding prefetch links to the HTML files. The HTML code on this website adds up to a total of 469K at the moment, so prefetching links should make navigating the page much smoother.

The new logo for my website.
The new logo for my website.

For the sake of readability I use colours very carefully on my site. All text is black, and most backgrounds are white (with tables and code listings with grey background as notable exceptions). However, a five-minute-Inkscape-job produced a bit of colour, in the form of an icon. This now decorates the titles of my pages. The “for all”-symbol () is one of many decorative symbols used in mathematics.

Simple websites

From the start, the idea behind this wabsite was to make it simple and functional. At first my though was: Simplicity and functionality should go hand-in-hand. The assumption being that the designers of HTML and web-browsers should have made it so that the simplest solution is allways functional.

No, actually I didn’t actually think so – because I have seen webpages which are just simple HTML, and they are not functional: by default Firefox renders HTML without any further styling with full screen length lines in a tiny font. So I knew that I would have to put some effort into making a simple yet readable website.

The biggest time-saver when working on this web-site is Pandoc. Writing the page in Markdown instead of HTML saves a lot of time.

Here is something Pandoc’s HTML template contains, which I would not have guessed on my own:

<meta name="viewport" content="width=device-width,
  initial-scale=1.0, user-scalable=yes">

This magic incantation makes my website look normal on smart phones. Without it, the browser on the phone will zoom all the way out, making the text unreadable without zooming in. Why this is the default behaviour escapes my understanding.

In general the HTML generated by Pandoc holds high quality, and is very easy to style using CSS. And when it comes to CSS, a little can go a long way:

While design is some part of functionality, it is not all. For instance, you should have some way of checking that the links on your website actually work. It is easy to mistype a URL, or maybe the link dies after you publish it. I hacked together a mkfile-target for this purpose, which uses curl to check each link:

links-check:QV: `{grep -v '/$' $index | grep '\.html$'}
  if (~ $base '')
# Get the absolute path for base
  cd $base
  cd $wd
# Get the search and replace string for absolute server links
  ss='s/^\//'`{echo $base | ssam -e 's/\//\\\//g'}^'\//g'
# Iterate through html files and check remote links with curl
  for(i in `{grep -v '/$' $index | grep '\.html$'}) {
     cd $base
     newdir=`{echo $i | ssam -e 'x/[^\/]*$/ d'}
     if (! ~ $newdir '')
        cd $newdir
     for (u in `{ssam -e 'y/href\=\"[^"]*\"/ d' < $base/$i \
               | ssam -e 'x/href=/ d' \
           | ssam -e 'x/\"[^\"]*\"/ y/[^\"]*/ c/\n/' \
           | grep -v '^$' | grep -v '^#' | grep -v '^data:' | grep -o '^[^#]*' \
           | ssam -e $ss } ) {
        if (! test -e $u)
           if (! curl --http1.1 -k -s -r 0-255 -o /dev/null $u) {
              echo $u is invalid in $i
              cd $base
              exit 1}
     cd $base }

The part about --http1.1 in the curl line is just a work-around for some faulty HTTP/2 sites.

2019–03–02, Saturday

Back from Oslo, where I gave a talk at CAS (slides).

Home in Bergen, we had wonderful weather yesterday, but today it was back to more familiar 2°C and sleet. Didn’t stop me from enjoying our balcony, which is glassed in and heated.

On the balcony, I am watching a series called Molten Modular on YouTube. The series, in addition to being a fabulous show of shirts, is a pleasant intro to EuroRack. The thing is that Robin Vincent, the creator of the Molten Modular series, is learning modular synthesis as the series goes along. This kind of learning from beginners has its pros and cons, but as long as one keeps a positive, critical attitude, it can stimulate one’s own learning very well.

2019–03–16, Saturday

Add two tracks to my list (007 and 008). Both are just recordings of me playing with patches. I like both patches, but for different reasons.

The first patch is perhaps most insteresting: There are three oscillators on it, each one playing different tones from a chord. They each walk through the chord, but always separated by 90° on a triangle wave. Then the sounds are mixed in everchanging porportions. The prominent effect is a low-pass resonance filter, where the resonant frequency is on a saw shaped LFO. This give the cyclic drops which give a somber beat to it. There is a bit of FM thrown in for flavour, and my favourite LADSPA canyon delay (from the cmt package) sits at the end.

The second patch was fun to play. It is just the AMS random module at high speed playing two oscillators. It switches between minor and pentatonic, which gives the patch some life. For this patch I had my MIDI controller connected to transpose the oscillators and one of the bottons basically controlled on or off the high pitched solo voice you can hear. The track is basically me playing that one botton like a rock star guitar hero, and even though there are a lot of imperfections in this track I decided it needs to be uploaded.

Last year, I bought a Omnitronic FAD.9 MIDI controller, and I have found surprisingly useful – not just controlling parametrs for modular synths, but also to control jack_mixer. In my setup I have jack_mixer as the main mixer of my system. So I can use the FAD.9 to control the volume both from JACK native programs (such as Audacious, Audacity, Alsa Modular Synth and Rosegarden).

Now the only thing I am missing is a plugin for Audacious which lets me use some of the buttons on the FAD.9 to control the music playback, and I will be back to the kind of setup I had in my teens: Then I had a joystick controlling Winamp, and it was the best music experience ever. I could play Unreal Tournament while listening to music, not having to swtich out of Unreal to change song.

2019–03–17, Sunday

Surfing defensively.

  1. For my part, it this is an overstatement, but this guy has actually walked them all.

  2. who is also on SoundCloud and currently works on Lawdle

  3. The unit em is a relative unit, useful for making the page scalable

Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺