Comment by dbaupp

A model that just talks about "the first N elements of this allocation are initialized" or even "this contiguous subsequence is initialized" is very limiting. E.g. it doesn't allow for a ring buffer, nor a hashmap that leaves some locations uninit.

I don't see how baking special cases for safety into the compiler is any better than having more general tooling, and constructing safe wrappers in Rust.

Also, just for some context, you're often complaining that Rust is too complicated comparing it to C++. Your desires for extra power to reason about pointer-soups (or writing inductive proofs in the language, rather than using existing tooling for it) aren't going to fix that at all, and indeed are likely to add a whole extra level of complexity.

It doesn't seem like a good use of time, or "language-complexity budget", to have the language features that specifically allow `Vec<T>` to be implemented safely, when that can all just be done in (not-that-complicated) normal Rust code. Additionally, reasoning about code (i.e. feeling satisfied in its correctness) is almost always easier than reasoning about code that reasons about code (i.e. feeling satisfied that the proof-checker/compile will correctly prove other code's correctness).