Essay archive
A chronological notebook on software engineering, programming languages, program analysis, formal verification, and everything in between.
2026
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.