Linear types (and affine types, as in Rust) only buy you some memory safety (preventing use-after-frees, and memory leaks although that's not really a safety is

Linear types (and affine types, as in Rust) only buy you some memory safety (preventing use-after-frees, and memory leaks although that's not really a safety issue). The more important part of memory safety is preventing out-of-bounds accesses. Rust, Ada, and (it seems) Beef sacrifice performance for memory safety here by having runtime bounds checking. (Though there is not much performance cost to this and all of those have options to turn off runtime bounds checking anyway.) The only performance-oriented language I'm aware of that is fully memory-safe at compile time is ATS‚ via a combination of linear types and dependent types, and using ATS is… cumbersome.