In practice Rust's type checker accepts only a _very_ small subset of correct programs. I've been in a position to write some decent sized Rust code recently and it takes a shift in your mindset to start writing decent Rust code.
Even now there are patterns I'm unsure how to model in Rust. Arena allocation is a good example because it was partly the cause of Heartbleed too. Arena allocation in rust seems to require unsafe pointers and unsafe code blocks. You can look at Rust's standard library and see this.
2. The point being that the Rust language exposes unsafe code blocks and pointers. At some point you're going to hit those blocks (if nothing else in 3rd party code) and you're back to square one: You need to trust unsafe code that it is correct. It doesn't matter if that code is a VM or unsafe code.
*edited for some legibility.
What does matter is the amount of unsafe code to trust. It's much easier to check that a small area of clearly-marked unsafe blocks does "the right thing" than if your entire program is a gigantic unsafe block.
To me it makes sense. And the example you give here is very relevant. First you'd try to do it within the standard language bounds and only when you realize you can't do it that way, I'll resort to unsafe code. But now your very aware that this part of the code needs to be treated why extra care. So, to me, you're not completely back to square one.
Nicholas Matsakis make this very point near the end of this talk: https://www.youtube.com/watch?v=9wOzjbgRoNU
I would even add, if care is taken to make that unsafe code really small it can even been generated by Coq for instance as stated in some comments here.
That said Rust might not be the best out there for the job but IMHO it shouldn't be dismissed to fast either. It is similar enough to C++ to allow a less painful transition for devs with the domain knowledge.
Of course such a project must require extra scrutiny on all level and Rust does not resolves all the problems. I'd say pick your battles. Rust provide some interesting middle ground between C/C++ and a completely different language like Ada.