Yes, it’s time to redo my blog again. This time I found an ultra light-weight blog theme. This page here is under 100KB! I wanted to make something that acts more like a homepage for my research, rather than a blog. I still have all my blog posts, but now the focus will be on a more professional presentation of my work. This theme is really what I’ve wanted all along: a home page with a max-width for the text, table of contents, and built-in local search! ...
It's hard to overstate how important email is in our modern world. Even as hip new platforms like Slack &co. gain traction in the workplace, so much communication takes place in a crusty old medium that's outlived every purported "email killer". Where does it get its staying power from? Email predates much of the Internet as we know it today. Its current incarnation first emerged in the early 80s, though it has roots in earlier forms of digital messaging from as far back as the 60s. ...
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. ...
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. ...
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. ...
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.
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. ...
μ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. ...
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. ...
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. ...