> provably safe

There's the thing.

The reason that some problems can simply be solved more efficiently (on current hardware architectures) in C than in other languages is that there's a difference between what is "provably safe" and what is "provably safe to a compiler". That's the whole point of Rust's unsafe{}; not to write code that's actually unsafe on purpose, but to say, "this code is safe, even though you can't prove it" (indeed, perhaps unsafe blocks ought to be renamed to safe blocks; that would also alleviate the problem of opposite meanings of unsafe blocks and unsafe functions).

That is to say, it's not true that there are data structures impossible to write in a provably safe way without automatic GC, since whatever automatic GC can do the programmer can do too (although, admittedly, at some point one begins to blur the line between GC and manual freeing, such as with reference counting). It's just that it's a lot easier for the compiler to prove that GC-managed code is safe.

I'm not sure that being forced to have the compiler prove that your code is safe rather than being able to say, "no, I proved it myself with more advanced techniques" is a good thing. Admittedly, most programs written today in so-called "safe" languages are probably beyond the scope of their programmers' abilities to prove safe, but then again, a lot of those programs turn out to be horribly unsafe even with the compiler's help!

  > perhaps unsafe blocks ought to be renamed to safe blocks

We have had long and heated discussions on this topic, actually. My personal position is that the code inside such a block has fundamental tension: the compiler must assume that it is safe, while the programmer must in all cases admit the possibility that it is unsafe. Given that keywords should be optimized for the reader rather than the compiler, I prefer `unsafe` to `safe`.

However, that's not to say that there doesn't exist a better word entirely. Perhaps `unchecked` would suffice...