I am pretty sure this is the same mistake I was making and is addressed by @eternaleye here (see the code sample in that post). The key is that an invariant should be true throughout the whole execution, whereas a pre/post condition does not have to be.
While I agree with the overall motivation, I respectfully disagree that this is the right approach... Rather, I think that the right approach is to do a better job at teaching about unsafe. When I was learning Rust, I was never unclear about when to use an unsafe
block. In fact, I was never confused about unsafe
until I had to start designing interfaces that use unsafe
. At that point the question arises: "Should interface X be unsafe
?". Perhaps there is a syntactic change that would make that more clear, but I don't know what it is.