I've spent about ten years building software for a living, including a couple of products I built from the ground up.
I love type-driven design and use it wherever I can. Making invalid states unrepresentable has been a big driving force in my career. I moved from JavaScript to TypeScript for that reason, and from there to functional programming, which I've since written professionally in F#, Elm and OCaml.
Somewhere around Elm I started wanting to build a type system of my own. I've made a few attempts since, with varying success, and that's how I ended up using Lean, building small languages and proving things about them. Some of the results are below.
An interactive playground for building, exploring, and simulating interaction nets and Lafont's interaction combinators.
Dutch for tree. Lean 4 formalisation of triage tree calculus.
Verified, kernel-reducible reachability and shortest walks for finite directed graphs in Lean 4 + Mathlib.
Idiomatic F# library for the AT Protocol (atproto/Bluesky).
inner-ear — a little utility I made for my own use: your Mac's own sound as an input any app can use, so Screenshot (⌘⇧5) can record system audio. No audio driver needed.
Recordings of live sessions where a friend and I prove theorems in Lean 4 together, with chat joining in. On YouTube.