11 Aug 2022
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.
...
1 Aug 2022
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.
...
27 Jul 2022
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.
...
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.
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.
...
4 Jul 2022
μ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.
...
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.
...
2 Mar 2022
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.
...
18 Dec 2021
A collection of what worked well and what didn’t in classes that I took this semester. This is partially for me to record what things reduced friction for me as a student so that one day, should I become a professor, I’ll be able to run the lowest-friction class ever!
...
7 Dec 2021
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:
...