C can do exactly the same, it just won't perform the lifetime checks for you. I haven't written much Rust, but if I understand correctly you can write code that

C can do exactly the same, it just won't perform the lifetime checks for you. I haven't written much Rust, but if I understand correctly you can write code that is valid, but won't compile because you're not 'following the rules' of the constraints/type checker. I find Dafny to be a more elegant and nice solution, since this language allows you to actually prove your code is valid when it's not obvious from the static analysis. But this might be because I'm somewhat more mathematically inclined (and i admit that Dafny is still by no means easy to use)