Programming languages · Static analysis
Language design, ownership, and the proofs between.
Essays by Duckki Oe on the rules underneath software: how languages express intent, how references behave, and how static analysis can make those guarantees precise.
From the notebook
Latest essays
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.
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