>I recommend watching the video @nerditation linked. I believe Amanda mentioned somewhere that Polonius is 5000x slower than the existing borrow-checker; IIRC the plan isn't to use Polonius instead of NLL, but rather use NLL and kick off Polonius for certain failure cases.
>There is no reason a language like Rust can't be designed with much more sensible strict aliasing rules.
The aliasing rules of Rust for mutable references are different and more difficult than strict aliasing in C and C++.
Strict aliasing in C and C++ are also called TBAA, since they are based on compatible types. If types are compatible, pointers can alias. This is different in Rust, where mutable references absolutely may never alias, not even if the types are the same.
Rust aliasing is more similar to C _restrict_.
The Linux kernel goes in the other direction and has strict aliasing optimization disabled.
And TBAA is much easier for programmers to wrangle than the aliasing of Rust, right? The corresponding aliasing feature for C would be _restrict_, which is rarely used.
Though Linus and Linux turns off even strict aliasing/TBAA.
In C, you can alias pointers if they have compatible types. Not the case in Rust for mutable references. And the rules of Rust have tripped up even senior Rust developers.
Without MIRI, a lot of Rust developers would be lost, as they do not even attempt to understand unsafe. And MIRI cannot and does not cover everything, no matter how good and beloved it is.
It should have been possible for senior Rust developers to write UB-free code without having to hope that MIRI saves them.