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
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.
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