My name is James Kay. I like syntax, semantics, programming languages, natural languages, formal verification, and other things, and I work in the tech industry.

November, 2025

Letting the future out of the box

the problem of boxed futures in Rust, and three recipes to avoid them

Introduction

Rust is breaking new ground with unboxed futures — trying to build an async/await system that doesn’t mandate pointing into the heap. As such, it’s not unusual to run into problems where what would be a single Promise interface type in other languages is actually a slew of different implementation types in Rust. When this situation occurs it’s tempting to stick them all in a box and be done with it. Unfortunately, due to the way Rust handles trait objects, this can make things more complicated down the line. Let’s look in detail at the consequences of that decision, and explore other patterns we can use instead.

July, 2025

Ergonomic keyboarding with the Svalboard

a half-year retrospective

My background

Even before I started pressing buttons for a living I was always a pretty heavy computer user. When I was about 18 I started experiencing symptoms of RSI. At around the same time I learnt of the Dvorak keyboard layout, and so I switched, hoping it would solve my problems. It did, at least at the time, and so for the last 17 years I’ve been a Dvorak user.

September, 2023

Nix patterns I

separate your inputs and outputs

Introduction

I’ve been using Nix and NixOS for many years now, both personally and professionally, on workstations and servers. While the tools aren’t without their warts, I strongly believe the model espoused by Nix for package management is a leap ahead of other available tools. However, the Nix language can be very unstructured, and knowing how to use it in an effective and composable way can involve a lot of searching and deep-diving through nixpkgs. This series aims to collect patterns and good practices I encounter or devise, significantly for my own future benefit, but hopefully other people will find it helpful too.

August, 2023

The art of binding

variables made complicated

Introduction and pedantry

In programming, we typically think of a variable as a location to store a value. It turns out this is mostly an implementation detail; if we generalize them into their interface, we find a rich space of languages that captures the distinctions between several different types of programming language that seem very different at first glance.

February, 2023

λ-calculus for programmers

programming language fundamentals

Introduction

If you’ve done much functional programming, you’ve probably heard of the λ-calculus, invented by Alonzo Church in the 1930s. If you haven’t, the term might be quite new to you; but don’t worry, despite the intimidating name the λ-calculus is actually very simple.

January, 2023

Linear types for programmers

reasoning about resources

Introduction

Linear types are an application to type theory of the discipline of linear logic, first described by Jean-Yves Girard (Girard, 1987). Since its inception it has led to many fruitful discoveries in computer science. In this article I hope to explain why it is so interesting, as well as relate it to concrete tools and practices available to programmers today.

November, 2021

Site design & construction

philosophy and realization

Design

I often focus too hard on the design of websites to the detriment of the content, so the design of this site was intended to front the content. Originally I didn’t even have a title on pages, but I’ve never been able to pass up the opportunity for a subtitle…

October, 2021

Lorem ipsum dolor sit amet — consectetuer asciidoc elit

donec hendrerit tempor tellus

Lorem ipsum

Lorem ipsum dolor sit amet, consectetuer adipiscing elit. Donec hendrerit tempor tellus. Quis donec pretium posuere tellus. Proin quam nisl, tincidunt et, mattis eget, convallis nec, purus. Cum sociis natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus. Nulla posuere. Donec vitae dolor. Nullam tristique diam non turpis. Cras placerat accumsan nulla. Nullam rutrum. Nam vestibulum accumsan nisl.