This is my public diary.
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.
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.
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 Дед Мороз.
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:
email@example.com $ newmail hub.darcs.net firstname.lastname@example.org
And if you later forgot which one you had generated:
email@example.com $ whichmail hub.darcs.net firstname.lastname@example.org
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.
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.
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.
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.
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.
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.
For my part, it this is an overstatement, but this guy has actually walked them all.↩
who is also on SoundCloud and currently works on Lawdle↩
The unit em is a relative unit, useful for making the page scalable↩