Projects
Over the course of my life I’ve made cool stuff. Here I’ve documented a mix of things I consider cool because people use them, and things I consider cool because they’re technically interesting solutions to esoteric problems. I have a tendency to not finish my projects, especially beyond overcoming a significant challenge (the crux of the problem), or when the project turns into tedium.
- Sandbox
- finite-typelits
- The Powder Toy
- Coq Classical Ensembles
- CompaREST
- BOOTSTRA
- De-Rham Curve Renderer
- Doger
- kbdtop
- DLNG
- OS
- Universal Machine Emulators
- Dequantify
- Lua Scripting Support for HexChat
- functional-kmp
- Floppy Drive Midi Player
- xsTPTIRC
Sandbox
A long time ago I was running an IRC1 bot that would let strangers on the internet run arbitrary pieces of code, for testing/demonstration/learning purposes. In order to protect the host of the bot from obvious vulnerabilities I made a process sandbox based on ptrace, inside which the untrusted code would run. Originally employed by an IRC bot for the #lua and #haskell channels, it is now mostly used by a Discord bot for the Functional Programming Discord server.
finite-typelits
I maintain a somewhat widely-used Haskell library for types with a finite number of elements specified at the type level using GHC’s first-class type-level numbers.
The Powder Toy
The Powder Toy is an oddly famous falling sand game, which I’ve helped develop. In the early years I made a lot of improvements to the Lua console, and in the latter years I’ve mostly helped refactor the game into more modern C++.
Coq Classical Ensembles
I’ve implemented a library for the Coq proof assistant for manipulating classical (excluded middle) sets, represented type-theoretically as predicates on a given universe. The original intent was to use it to in turn make a library for general topology.
CompaREST
Ever wonder what changed between two versions of an OpenAPI schema, and whether the old client would still work with the new server? As part of my work at typeable.io I wrote a static analysis tool that does just that: it’s called CompaREST, and it’s free software!
BOOTSTRA
Could you bootstrap a programming environment from a clean MS-DOS install having nothing but documentation? I sought to find out.
The first chapter of the story was to write an assembler that was better than the one available in DEBUG.EXE, in that it would support labels. And so I wrote a complete 8086 assembler in MS-DOS batch, a language with virtually no string processing utilities. This was done by interpreting the input assembly as a batch file which would call subroutines for various 8086 instructions.
The next chapter was to write a compiler for a slightly higher level language using this assembler. To that end I implemented a stack-based procedural language with module support.
The next step would be to reproduce a system for separate compilation that could link “object” files into an .EXE file, but I got bored by then.
De-Rham Curve Renderer
I made a standalone program that calculates a polyline approximation of arbitrary iterated function systems — a class of fractals, of which de Rham curves are a common subset.
Doger
I developed and hosted the IRC1 tipping bot for the cryptocurrency Dogecoin. It was called Doger, and was listed as one of the official Dogecoin bots. In retrospect I can say that this is NOT how you should implement a monetary transaction system.
kbdtop
If you have an MSI per-key RGB keyboard, you can display htop-like system resource usage on it using a little C program I wrote.
DLNG
In the modern world there’s fewer and fewer reasons for a program to have hot code reloading, but back in the era of IRC1 bots that was a big deal. You could employ dlopen and friends to dynamically load shared objects as “plugins” in your program, but what about reloading the main loop? What about reloading the reloader? I’ve set out to write a replacement for the run-time dynamic linker (also known as ld-linux.so, the provider of dlopen, usually part of your libc) with a more fine-grained interface that could achieve exactly this kind of functionality. It was called “Dynamic Linker NG”. I never got to the reloading part, but I did manage to successfully use it as a program interpreter for unsuspecting programs.
OS
Like everybody and their dog, I’ve tried my hand at making my own “OS”. I ended up with an MBR-bootable program capable of running a Lua shell with a persistent filesystem, and for it a simple text editor written completely in Lua.
Universal Machine Emulators
I found out about the 2006 ICFP programming contest way later than it actually happened, but I was enamoured with the idea of it. You had to write an emulator for a made up processor architecture, and then run an unknown program on it — which turned out to be a full Unix-like operating system. In the pursuit of efficiency I ended up writing a JIT binary translator for this ISA.
Dequantify
There’s an algorithm that can remove $\forall$ and $\exists$ quantifiers from statements involving polynomial arithmetic, for example, the statement $\exists x : x^2 + px + q = 0$ is equivalent to the statement $p^2-4q \ge 0$, which in turn has no quantifiers! This algorithm is a consequence of the Tarski–Seidenberg theorem, and it is impractically slow, but I have a Haskell implementation of it which I’ve used as credit in a formal systems class.
Lua Scripting Support for HexChat
I implemented Lua scripting support in HexChat, a popular IRC1 client, and it has since become the preferred way to write scripts for it. Originally a standalone library, it has since been merged into the HexChat source tree.
functional-kmp
The Knuth–Morris–Pratt substring search algorithm is normally implemented using arrays, and relies critically on $O(1)$ access that the array provides. However arrays aren’t “first-class citizens” in pure functional languages, as opposed to algebraic datatypes. It turns out it’s possible to re-engineer the algorithm to use cons-cell-based lists instead. A Haskell implementation of the resulting algorithm is available as a library on Hackage.
Floppy Drive Midi Player
Ever seen one of those videos where music is played on old floppy drives? A lot of them directly hook up wires to the stepper motors, but it turns out you can tell the Linux kernel and in turn the IDE bus to directly control the head of a floppy drive connected in the “normal” way. FDMP is a prototype of a program that can play MIDI files on a floppy this way.
xsTPTIRC
xsTPTIRC was an in-game IRC1 client for The Powder Toy. I was 14 when I made it, and it was one of the first things I wrote that other people actually used.