GC works great in practice, but as you say it isn't provable. Likewise, Rust goes a long way towards preventing deadlocks in practice, but that also isn't provable. All I'm talking about here are guarantees. Rust's type system guarantees that there are no data races; that's firm bedrock that I can rely upon. I can't rely on there being no deadlocks just as I can't rely on a garbage collector actually returning any memory. That doesn't mean these tools aren't useful in practice, only that I have to take their failure modes into consideration if I want to write correct programs.