A proposal for a memory-safe type system that sits between C++'s permissiveness and Rust's strictness. The core idea uses flow-sensitive typing with linear ownership: when a value is conditionally dropped, the compiler automatically widens its type to Option<T> rather than rejecting the program outright. Developers must then explicitly narrow (refine) the type before use, enforced at compile time with a single runtime check only when static proof is impossible. The system introduces Some<T> as a non-owning proof-of-availability type, and is grounded in flow-sensitive typing, refinement types, and abstract interpretation. It claims to eliminate the same bug classes as Rust (use-after-free, dangling pointers, memory leaks, etc.) while being more ergonomic, and is implemented in the author's own programming language.
