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

I work on formally verified combinatorial auctions and market infrastructure at OneChronos. (We're hiring)

• Zero to QED (2025) - Interactive theorem proving in Lean 4.
• Typechecker Zoo (2025) - A collection of type system implementations in Rust.
• Compiler Crates (2025) - Examples of crates for building compilers in Rust.
• Introduction to MLIR (2024) - A short introduction to building compilers on the MLIR infrastructure.
• Tiny GraphRAG (2024) - Building a minimal graph-based RAG system.
• Exotic Programming Ideas (2021) - Exploring unusual programming language concepts.
• Quirky Nerd Humour (2020) - Satirical articles about programming culture.
• Write You a Haskell (2015) - Building a Haskell compiler from scratch.
• What I Wish I Knew When Learning Haskell (2009) - A comprehensive guide to Haskell.

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