What is realizability?

:: research, notes, academia

I recently decided to confront the fact that I didn’t know what “realizability” meant. I see it in programming languages papers from time to time, and could see little rhyme or reason to how it was used. Any time I tried to look it up, I got some nonsense about constructive mathematics and Heyting arithmetic, which I also knew nothing about, and gave up.

This blog post is basically a copy of my personal notebook on the subject, which is NOT AUTHORITATIVE, but maybe it will help you.

The A Means A

:: research, academia

I have argued about the definition of “ANF” many times. I have looked at the history and origins, and studied the translation, and spoken to the authors. And yet people insist I’m “quacking” because I insist that “ANF” means “A-normal form”, where the “A” only means “A”.

Here, I write down the best version of my perspective so far, so I can just point people to it.

What is peer reviewing?

:: academia

I’ve been doing, and experiencing, a lot of peer reviewing lately. I’ve been ranting about it on Twitter as I get reviews that don’t help me and, in many ways, hurt me, and lauding reviews that provide useful constructive feedback (even if I disagree with it or the decisions). I’ve been trying to figure out how to provide good reviews and avoid negative aspects of reviewing.

I need to get the thoughts out of my head. These are not declarations of what peer reviewing is or should be, but my attempt to work through those questions.

What is the Point of a Final Exam

:: academia

It’s weird, but professors are almost never taught how to teach, how to design a course, how to assess students, how to design an exam or what the point of an exam even is. We’re just expected to pick this up on our own, I guess. It’s not as nonsensical as it sounds, since we are trained how to do research and communicate that research, and there is some overlap. But still.

If my experience is any indication, we just pick up an existing course structure and more or less follow that. Oh, the last person who taught this course used this material, and this syllabus, and these exams, so I’ll just do more or less that for now. If we’re ambitious and/or want to shoot our tenure track in the foot, we might try to innovate soon after. Otherwise, we might innovate later.

Anyway I’m not good at doing things just because that’s how they’ve always been done; I need first principles. After designing, administering, grading, invigilating several of them, I was struggling to figure out what the point of a final exam is. So I had a bunch of conversations on Twitter and now I’m collecting my thoughts on what the point of a final exam is and how it might, or might not, serve a purpose in my course.

Warning: I am not an education researcher, and this is not research, and it’s got a lot of stream-of-consciousness.

Enabling CORS for nginx WebDAV and CalDAV reverse-proxy

:: linux, tricks

The past few weeks I’ve been learning to develop and deploy a Progress Web App (PWA) that can communicate with my WebDAV and CalDAV servers. Unfortunately, while these are on the same domain, they are on different sub-domains, and this causes the requests to be considered cross-origin requests. For security reasons, cross-origin requests are blocked by most browsers by default unless the server explicitly allows cross-origin resource sharing (CORS). This is pretty easy to set up for static resources or scripts, if they use default headers and GET and POST methods. However, it’s particularly complicated for WebDAV, CalDAV, and other protocols that use additional headers or methods.

A Suitable Cutlery Tray

:: memes

This post is a transcription of a thread that happened live on Twitter on June 30, 2019, in response to some anger at my lack of a cutlery tray. I was in a mood following a previous cutlery incident.

What is the optimal arrangment of cutlery in a drawer?

:: memes

This post is a transcription of a thread that happened live on Twitter on June 30, 2019, in response to someone claiming there was a correct way to arrange cutlery in a drawer. The statement caused me to momentarily lose my mind. The thread has since become difficult to find, so I’m reproducing it here.

Locking down your browser to defend yourself from rickroll

:: tinkering

Recently, a UBC SPL grad student offered a bounty to anyone who could Rickroll me. This has resulted in an arms race. I have increased my browser security to prevent Rickrolling entirely on most of my machines. This isn’t fool proof, of course, but hopefully it will help defend against low-tier attempts.

Setting up your backup service

:: linux, tricks, tutorial, optimize everything

I just ran the command rm -rf ~, deleting all my personal files in the process. This was not the first time, and it was no big deal, because I back up my files with automatic rolling backups. My backup system is secure, redundant, and has low resources requirements. The backup repository is encrypted, deduplicated, compressed, and mirrored across multiple machines. You can choose to use any or none of these features while following this guide.

In this guide, I describe how to set up a secure and robust backup service yourself, which runs on Linux, macOS, and Windows via WSL 2. I provide my own scripts, config files, and workflows for maintaining, validating, and restoring the backups. This is all setup using free software, supports multiple configurations with varying degrees of security and redundancy, and scales well to more backup clients.

If you’d prefer to not set this up yourself and you run macOS or Windows, I recommend Backblaze:


They automatically handle everything, including most of the features I want in a backup service and some I could never implement myself, for $6/m per machine (USD).