> value performance over total memory safety

Is there any evidence this is a tradeoff? What of linear types?

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.

> Rust, Ada, and (it seems) Beef sacrifice performance for memory safety here by having runtime bounds checking

Its not all black and white though. Using iterators, bounds checks can often be elided by the Rust compiler.

> Is there any evidence this is a tradeoff?

Bound checking often is the reason rust performs worse on some benchmarks. Though I wouldn't consider this a problem at all since it can be disabled.

It's better to manually hoist the bound checks so that they happen before any critical loop. The compiler often can't do this because it has to preserve the partial effects of where the failed bounds check happens, but that's generally not what you really want; if anything, you'd rather fail fast.

leaks aren't unsafe though. Things like bounds checking and aliasing guarantees are like 90% of the memory safety issues you care about, and those can be performant.