Essay archive
A chronological notebook on programming languages, reference semantics, ownership, and static analysis.
2026
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.