navigate: home • resume • blog
my professional work spans formal verification, systems programming, programming language design, and generally applying mathematical rigor to make computers actually work reliably. my unprofessional work includes strategy and resource management games, web culture, and inhaling incredible amounts of science fiction.
major projects
abstract strategy games → theory & implementation
a collection of game implementations, usually in Rust. some are more developed than others.
absass RISC → FPGA implementation
a fun summer hack: designed and implemented a simple RISC ISA in multiple HDLs, achieving single-cycle retirement at 240MHz on FPGA. includes compiler, emulator, assembler.
ICFP 2020 contest → competitive programming
overengineered-for-fun high-performance functional programming with combinator-based approach and concurrent garbage collector implementation.
rust language — compiler • community building • core tooling
pre-1.0 contributor. created the first version of the currently-shipped rustdoc, spec'd and implemented the flexible target specification system for cross-compilation, started This Week in Rust, and kicked off VisualRust. cargo-lite, gl-rs, and more.
mina protocol — founding engineer • zkSNARK blockchain
founding engineer at O(1) Labs working on Mina during its birth. mina is a hash-linked distributed proof system that leverages advanced constructive mathematics to make blockchain history manageable. i did peer-to-peer networking, storage management, protocol design, consensus development, and build system/packaging. i was excited about the possibilities of zero-knowledge proofs.
robigalia & seL4 — research • formally verified systems
work on seL4, the first kernel with a computer-checked end-to-end correctness proof. created Robigalia, a persistent capability OS design using rust.
themes
across these projects, several themes emerge:
- formal methods: using mathematical proofs to ensure software correctness
- capability-based security: making security properties explicit and compositional
- type systems: leveraging static analysis to prevent errors
- developer experience: building tools and infrastructure that make complex systems accessible
- correctness by construction: designing systems where bugs are impossible rather than caught after the fact
the unifying goal is making computers actually work: building systems that are provably correct, secure by design, and understandable by humans.