I've spent about ten years building software for a living: front ends, back ends, and a couple of products from an empty repo.
My favourite bugs are the ones that can't be written. I lean hard on type-driven design and making invalid states unrepresentable, which is what moved me from JavaScript to TypeScript and then on to functional programming. I've since written F#, Elm and OCaml professionally.
Elm gave me the urge to design a type system of my own. I've had a few goes since, with mixed results, and that's how I ended up learning Lean, building small languages and proving things about them in my own time. Most of the projects below came out of that.
These days I build a lot of it with coding agents. I set the architecture and make the design calls; the agents do most of the typing.
A browser playground for interaction nets and Lafont's interaction combinators. Wire up a net, then watch it reduce step by step, with every rewrite animated.
A small Elm-flavoured language, formalised end to end in Lean 4. It's proved type-safe, its inference always finds the most general type, and the verified code is the same code that runs your programs.
Dutch for tree. Tree calculus in Lean 4, a tiny model of computation where programs and values are all unlabelled binary trees. Any term can be drawn in the editor as a tree you click through, one proven-sound rewrite at a time.
Reachability and shortest paths for finite directed graphs, proved correct in Lean 4. The search is simple enough for Lean's kernel to run, so facts about small graphs are proved just by computing them.
A native F# library for Bluesky and the AT Protocol, built on types generated from the protocol's own schemas. Posts, likes and follows each get their own type, so mixing them up won't compile, and every call returns a Result instead of throwing.
inner-ear turns your Mac's own sound into an input any app can record from, so Screenshot (⌘⇧5) can finally capture system audio. No audio driver, and about a hundred lines of Swift. I made it for myself.
A friend and I proving theorems in Lean 4 live, with chat chipping in. The recordings are all on YouTube.