Essay archive
A chronological notebook on software engineering, programming languages, program analysis, formal verification, and everything in between.
2026
A Rust Engineer's Guide to Lean
Read Lean through familiar Rust concepts, follow a small proof, and learn how to review formal specifications and use a verified model in a Rust workflow.
Formally Verified GraphQL Incremental Delivery
Formalizing GraphQL incremental delivery in Lean exposed a missing WorkQueue contract, produced correctness proofs, and uncovered bugs in GraphQL.js.
Formalization-First Development: What Should Humans Review?
An experiment in turning a paper algorithm into a Lean specification, a proved floating-point implementation, and tested Python and Rust ports.
Static Analysis for GraphQL, Verified in Lean
A reusable framework for sound and precise GraphQL query analysis, with an IBM cost model, optimality proofs, and an open-source Rust implementation.
Proving GraphQL Query Inclusion in Lean
A semantics-first theory and verified decision procedure for deciding when one GraphQL query includes another.
Introducing LeanFmt: A Code Formatter Written in Lean
LeanFmt formats Lean code with syntax-aware layout, leading operators, code-preservation checks, and support for project-specific syntax.
Auditing GraphQL Implementations With a Verified Model
A paired static audit shows how a Lean model can turn an open-ended GraphQL code review into a focused search for observable implementation differences.
Executing GraphQL Without CollectFields
A verified syntax-order GraphQL executor that avoids grouped field maps, plus a TypeScript implementation and benchmark against GraphQL.js.
When GraphQL Normalization Does Not Preserve Validation
Why semantics-preserving GraphQL normalization can produce an invalid operation, and what Lean proofs reveal about validation and execution.
Formalizing GraphQL and Proving Query Normalization in Lean
A Lean formalization of GraphQL execution, plus proofs that directive-aware query normalization preserves semantics and produces a canonical form.
2024
Inferred Mutability: Safety Proof of Mutability Upgrade
A sketch of the language rules and safety argument needed to upgrade an immutable reference to a mutable one.
The Properties of Reference
A vocabulary for separating reference uniqueness, exclusivity, ownership, and mutability—and reasoning about their relationships.
Inferred Mutability: A Cure for Rust's Mutability Madness
A proposal for inferring reference mutability from context to reduce duplicated accessor implementations in Rust-like languages.