A flow-sensitive typing approach to memory safety: single ownership, exactly-once destruction, and automatic Option promotion when liveness cannot be proven.