Hi there 👋

I'm a software engineer in London. I write about math and programming on my eponymously named blog.

I work on formal methods applied to combinatorial auctions and market infrastructure at OneChronos. (We're hiring)

Tech

Rust, Python, TypeScript, C++, CUDA, Haskell, OCaml, Lean

A functional language with algebraic effects, multishot continuations, and native codegen

Rust 159 8
A menagerie of cute implementations of modern typechecking algorithms

Rust 449 17
From Zero to QED: An informal introduction to formality with Lean 4

Lean 122 20
What I Wish I Knew When Learning Haskell

Haskell 2.7k 241
Bulletproofs are short non-interactive zero-knowledge proofs that require no trusted setup

Haskell 554 49
A toy compiler for NumPy array expressions that uses e-graphs and MLIR

Python 126 12