> Notice that the working approaches have something important in common: a strong system that, given certain assumptions, guarantees the lack of memory safety problems.
That's a very good point and I'm not arguing against it. It's just that even if it's true -- and I'm more than willing to concede that it is -- it still doesn't answer the question, which is: what is the best approach to achieving a required level of correctness?
The "soundness" approach says, let's guarantee, with some caveats, certain technical correctness properties that we can guarantee at some reasonable cost. The problem is that that cost is still not zero, and my hypothesis is that it's not negligible. My personal perspective is that Rust might be sacrificing too much for that, but that's not even what has disappointed me with Rust the most. I think -- and I could be wrong -- that Rust sacrifices more than it has to just to achieve that soundness, by also paying for "zero-cost abstractions," which, for my taste, is repeating C++'s biggest mistake, namely sacrificing complexity for the appearance of high-level abstraction that may look convincing when you read the finished code (perhaps more convincing in Rust than in C++), but falls apart when you try to change it. Once you try to change the code you're faced with the reality that low-level languages have low abstraction; i.e. they expose their technical details, whether it's through code -- as in C and Zig -- or through the type system, as in Rust. Zig says, since the abstraction in low-level languages is low anyway (i.e. we cannot really hide technical details) there is little reason to pay in complexity for so-called zero-cost abstractions.
Language simplicity goes a long way, even as far as sound formal verification is concerned. For example, there are existing sound static analysis tools that can guarantee no UB for C -- but not the complete C++, AFAIK -- with relatively little effort. It's not yet clear to me whether Zig, with its comptime, is simple enough for that, though.
It is my great interest in software correctness, together with my personal aesthetic preferences, that has made me dislike language complexity so much and made me a believer in "when in doubt -- leave it out."