A personal notebook by Duckki Oe
Software engineering, programming languages, formal verification, and everything in between.
I write about the ideas and tools that help us understand software more precisely—from language design and program analysis to mechanized models and verified systems.
From the notebook
Latest essays
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.
Read essayStatic 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.
Read essayProving GraphQL Query Inclusion in Lean
A semantics-first theory and verified decision procedure for deciding when one GraphQL query includes another.
Read essayIntroducing 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.
Read essayAuditing 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.
Read essayExecuting GraphQL Without CollectFields
A verified syntax-order GraphQL executor that avoids grouped field maps, plus a TypeScript implementation and benchmark against GraphQL.js.
Read essayWhen 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.
Read essayFormalizing 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.
Read essayInferred 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.
Read essayThe Properties of Reference
A vocabulary for separating reference uniqueness, exclusivity, ownership, and mutability—and reasoning about their relationships.
Read essayInferred 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.
Read essay