Until recently, I was a researcher at the Machine Intelligence Research Institute. Humanity is building AI systems to be subject to fewer constraints of the world, let’s not be subject to the AI systems either. I’m bushwhacking for moonshots that make this possible!

In the ancient times, I developed Fiat Cryptography which enables the majority of secure connections to the internet (the big prime numbers behind the https lock icon), reported the plurality of all-time bugs in the proof-assistant Coq (and joined the dev team to help handle them!), and contributed category theory to the Coq-HoTT library (hoorah for beautiful, unifying mathematics).

The compelling observation from these projects is that proof assistants are systematically slow, and if we expect verified security to scale as fast as we deploy software in critical infrastructure, we need to be engineering significantly more performant ways of generating and checking formal proofs. I wrote this up in a dense PhD thesis in 2020.

If the stakes weren’t so high, I would spend more time on cute maker projects, sailing, dancing, circling, and physics.