Rust's borrow checker implements substructural type theory (affine types), not a bolted-on safety net. Data has exactly one owner; borrowing enforces exclusive-write or concurrent-read access at compile time.
- Roots: Girard's 1987 linear logic, Baker's Linear Lisp, 1990s ownership-type work (Clarke, Noble et al.).
- Oxide (Northeastern, 2019) formally proved Rust's borrow discipline sound.
- MS and Google: ~70% of high-severity vulns are memory-safety bugs—eliminated at compile time by affine ownership.
- Android: memory-safety vuln share fell 76%→24% (2019–2024) as new code shifted to Rust.
- "Smart pointer" framing is misleading: ownership is a compile-time proof system, not a runtime trick.
- Roots: Girard's 1987 linear logic, Baker's Linear Lisp, 1990s ownership-type work (Clarke, Noble et al.).
- Oxide (Northeastern, 2019) formally proved Rust's borrow discipline sound.
- MS and Google: ~70% of high-severity vulns are memory-safety bugs—eliminated at compile time by affine ownership.
- Android: memory-safety vuln share fell 76%→24% (2019–2024) as new code shifted to Rust.
- "Smart pointer" framing is misleading: ownership is a compile-time proof system, not a runtime trick.
