Graphics engines, socket state machines, event-driven servers, parsers — built from the ground up, with correctness pushed into the type system through typestate and zero-cost abstractions.
"I enjoy problems where correctness is difficult to establish and failure is easy to hide."
My work focuses on making systems easier to reason about by replacing convention with explicit guarantees and replacing assumptions with enforceable structure. Whether building software or studying complex systems, I am interested in understanding not just whether something works, but why it continues to work under change, failure, and uncertainty.
My current work investigates Observable Insufficiency and Latent Resilience—the possibility that systems appearing to recover after disruption have not necessarily regained their original capacity to withstand future disturbances. Observable metrics may return to baseline while hidden structural changes continue to influence long-term behavior.
I explore this through computational modeling, graph theory, dynamical systems, statistical mechanics, and information-theoretic methods.
When is observable behavior an insufficient indicator of underlying correctness?
Passing tests does not necessarily imply soundness if invalid states remain representable.
Healthy dashboards do not necessarily imply healthy coordination.
Equilibrium does not necessarily imply resilience.
Across these domains, I am interested in reducing the gap between what a system appears to be and what it actually is. I am particularly drawn to problems where correctness, resilience, and recoverability can be expressed as formal properties rather than operational folklore.
// The connection's state lives in the type. The compiler enforces the protocol.
struct Socket<S> { fd: RawFd, _state: PhantomData<S> }
struct Closed;
struct Connected;
impl Socket<Closed> {
fn connect(self) -> Socket<Connected> { /* ... */ }
}
impl Socket<Connected> {
fn send(&self, bytes: &[u8]) -> Result<()> { /* ... */ }
fn close(self) -> Socket<Closed> { /* ... */ }
}
// socket.send(..) on a Closed socket is a compile error — not a 3am pager.
An experimental, math-first graphics engine with a type-safe rendering architecture and a Vulkan backend. The rendering pipeline's correctness is expressed in the type system rather than checked at runtime — geometry, transforms, and GPU state carry their constraints as types.
view repository →Models socket behavior as a type-level state machine. It explores how compile-time guarantees, typestate, and zero-cost abstractions enforce protocol correctness before the program ever runs — an operation that doesn't fit the connection's current state simply does not type-check.
view repository →
An event-driven server built directly on epoll — readiness-based I/O without a framework,
handling the accept/read/write loop against raw file descriptors to understand the machinery
async runtimes normally hide.
A JSON parser written from first principles — tokenizer to syntax tree, no parsing libraries. The groundwork for understanding how structured text becomes typed data.
view repository →A calculator in Rust — expression evaluation and the basics done deliberately. Small on purpose: a clean place to get the fundamentals exactly right.
view repository →