Technical Blog

Today I learned: Vertical monitors and subpixel anti-aliasing

11 Aug 2022
til, typography

Something I learned today from a coworker: if you turn your monitor sideways, subpixel anti-aliasing gets completely broken. This isn't as much of an issue on today's high-dpi displays, but for anything lower than a 4k screen, the effect can be noticeable. Just a little interesting thing I learned today. Thanks to my good, knowledgeable friend and coworker Jonner Steck! Also, while we're on the topic of font rendering, I've updated Iosevka Output to more closely match Input Mono: the cross-bar on the f now lines up nicely with the x-height. ...

A New Font

1 Aug 2022
happy-things, design, programming, typography

This week I created a custom build of the Iosevka font. I've used Input Mono for a long time now, and was very happy with it. However, it was missing a few glyphs that I wanted to use. Moreover, I didn't have a license for the Input font to use on e.g. my blog. Iosevka is stupendously customizable, so I thought I'd see if I could get something close to Input's styles. ...

How to write a type checker/type inferrer with good error messages

27 Jul 2022
tutorials, featured
programming-languages, type-checking, computer-science

All the source for this may be found on my SourceHut repository. Synopsis Experimental type checker/inferer for a simple lambda calculus Description This is a type inference system for a little language. (Described below.) It uses a fusion of type inference algorithms from PLAI, ESP, and μKanren. (See Resources) Broadly speaking, our type inference engine works by: generating typing constraints from the program solving those constraints We'll describe each of those in more detail. ...

Adding a Clock to the Tab-Bar in Emacs 28

20 Jul 2022

Today I figured out how to add a tab-bar to Emacs. I didn’t like having it in the mode-line: it gets duplicated for every window and my mode-line space is precious. In contrast, the right side of the tab-bar was always blank.

Rules for Social Media

17 Jul 2022

I’m not on many social media platforms these days. I like it like that. I mostly follow some academics and people who post interesting stuff. I post only occasionally, usually to show off my recent hiking exploits. I’ve come up with some rules for myself (all subject to change) about what I post. A post must meet all the following criteria: It must be positive and uplifting. There’s enough that’s negative on the internet. ...

microKanren Reading

4 Jul 2022
tutorials, featured
programming-languages, racket

μKanren (“micro-Kanren”) is a tiny, embeddable logic programming language. It’s easy to understand and implement in almost any language. It’s a great case study of an embedded language: unlike other common “embedded” languages like SQL or regex, which normally are represented as just plain-old strings, μKanren takes more advantage of the host language’s features. I recommend reading the original paper: it’s short, well-written, and easy to understand. I did a write-up which you can read on Sourcehut. ...

Blog update

2 Jul 2022

Brief update on the blog: I had been running a custom fork of the Anatole theme; it diverged pretty heavily, and I found a nice way to customize the CSS. Behold! The new-and-improved blog. Some of the new extensions to Anatole include the ability to set a static page as your profile; I’ll do this and include links to lists of publications and whatnot. This should make my blog a better place for my professional/academic life. ...

Complete and Liveness, Safe and Sound

2 Mar 2022
programming-languages, computer-science

I have a hard time keeping these terms straight: liveness vs. safety soundness vs. completeness This is intended as a short guide for myself; maybe someone else will find it useful too! Note that this is all to the best of my knowledge and understanding at the present time; if there be faults, they be the faults of myself. I welcome correction and clarification if I am wrong. Liveness vs. Safety # Liveness and safety deal with properties of a system. ...

Foundations of High-Modernist Ideology in Metropolis

7 Dec 2021
school, literature, literary-criticism

The following is from a essay from a class on German literature and film. Fritz Lang’s movie Metropolis is primarily about the struggle between the oppressed working class and the ruling elite. What drives this tension, however, is a particular view of technology and technological progress that exacerbates the problems the film focuses on. This mentality is called high modernist ideology by Scott in his book Seeing Like a State: ...