The answer isn't generics, Coq, or some fancy type system nobody will understand or use properly. There are only a few inherent trouble spots in pure Rust code safety. The big two are:
- Partially initialized arrays. "Vec" has to be unsafe because growing an array involves uninitialized slots. You just need a way to say "this array is initialized from 0..N only", where N is in a data structure associated with the array. Then you need an operation that says "initialize entry N+1 and update the count". That's all it takes.
"Map" could be implemented on top of "Vec", instead of using unsafe code. It would be worth trying this and seeing what the performance penalty is. That may be a premature optimization.
- Backpointers. Backpointers have an easily checked invariant relationship with the forward pointer that owns their containing object, but there's no way to tell the language that something is a backpointer.