A Grand Vision for Rust

Yoshua Wuyts, a prominent Rust contributor, outlines his ambitious vision for the language, focusing on three key areas to significantly enhance its safety and formal guarantees. His goal is to elevate Rust to the pinnacle of production-grade language safety, aiming for levels comparable to Ada/SPARK.

• Effects: Wuyts suggests formalizing and expanding Rust's support for "effect types," which are already present in async fn and const fn. This would allow functions to declare properties like guaranteed termination (no div effect), determinism (no ndet), or absence of I/O (io), providing stronger compile-time assurances for critical systems.
• Substructural Types: Building on Rust's affine type system (use at most once for memory safety), Wuyts proposes integrating linear types (use exactly once for memory leak prevention) and ordered types (use exactly once, in order, for stable memory addresses). These would further enhance memory safety and control, with ongoing work on traits like Move and Forget paving the way.
• Refinement Types: To address spatial memory safety violations (like out-of-bounds errors) at compile time rather than runtime, the vision includes "refinement types." Specifically, "pattern types" would allow annotating existing types with additional guarantees using Rust's pattern syntax (e.g., usize is 1.. for NonZeroUsize), while "view types" could permit mutable references to disjoint parts of the same data structure.

Wuyts expresses excitement for the ongoing formalisms and compiler improvements, driven by a personal mission to make Rust the safest production language available. He emphasizes that while these features may be complex to implement, they are ultimately worthwhile and intellectually stimulating.