Projects

Some Stuff I've Done

Note that most of these are messy because they were for educational purposes.

caspaxos

I wanted to dive into (lightweight) formal methods for program verification applied to distributed systems. CASPaxos is a relatively simple consensus protocol (or so we thought). So we decided to write a formal specification for it.

We have a complete spec, including an encoding of linearizability using quint, which is an implementation of the Temporal Logic of Actions (TLA+). Unfortunately, the linearizability invariant is blocked on a bug in quint, so we moved on.

While the goal was to learn about model checking, I also learned a lot about consensus.

BWOP

A stupid game inspired by the classic QWOP. Try to stay upright while your leg gets tired by only controlling the joints in your arms.

This was mostly just for fun, but it was also an exercise in using React and HTML canvas.

2ltt

An interpreter for a dependently-typed two level type theory. That is, it’s a (very!) simple dependently typed programming language that supports staged metaprogramming. Inspired by Kovacs’ Staged Compilation with Two-Level Type Theory.

The interpreter/elaborator uses Normalization by Evaluation (NbE) as the main evaluation technique, and does Staged Compilation to do the staging. It’s written in Haskell, because it makes it easy.

streamscl

There’s a cool research paper and library that implements stream fusion as a library using staged metaprogramming. As a Lisper, it was offensive that there was a cool metaprogramming thing that existed in another language that didn’t exist in CL. So I ported it to Common Lisp.

It basically works, though I didn’t get to implementing flatMap. It’s pretty cool, and is a relatively minimal implementation of a JIT compiler for an interesting domain-specific language embedded in Common Lisp.

There’s newer work out now, which I will look at eventually. (I implemented the POPL 2017 paper).

taglessfreeexperiments

Some educational explorations with different ways of writing interpreters (free monads, GADTs, tagless typeclesses) in Haskell, inspired by the Finally Tagless, Partially Evaluated paper.

I was concurrently working through Awodey’s Category Theory. Which helped give a lot of context with respect to things like initial and final encodings.

Spigot

A toy website that let’s you mess with stock-and-flow models from Complex Systems Theory. We made this to recreate the figures and analyses from Meadows’ Thinking in Systems, which is an interesting book by the way.

It’s written in vanilla javascript, with zero dependencies and no build step.

Scanner

A little program that exposes a linux compatible scanner over http. I run this on a raspberry pi 1b (I think) which is hooked up to the scanner over USB. It’s nice because network scanning kinda sucks, or did anyway when I made it.

The server is written in Common Lisp and is reasonably portable across implementations.

luajit-stapsdt

I was on a kick watching Bryan Cantrill talks, and learned about dtrace. I wanted to experiment with dyanmic tracing on my (linux) computer, and I was writing lua at the time, so I wrote a microlibrary with some ffi bindings to create probes accessible via ebpf.

Since I wrote it using the luajit ffi, the probes are genuinely lightweight because luajit can inline the calls.

Other stuff

I’ve worked on a bunch of stuff that isn’t here for various reasons, which if you meet me feel free to ask about! Here’s a sampling: