Two things comes to my mind immediately. Are there any known undefined behavior in the Rust language? Since UB is one of the most notable item that makes safety by compiler not a guarantee.
Also, how can we guarantee the compiler doing the check properly? Is it hard? My interpretation is that safety relies on the correctness of the compiler from that quote.
There are bugs in the implementation, but the language is specified to have no undefined behavior. (Note that some things are left unspecified, such as the memory layout of enums and vtables and the sorting algorithm that `sort` uses, but there is no undefined behavior in the C sense.)
> Also, how can we guarantee the compiler doing the check properly? Is it hard? My interpretation is that safety relies on the correctness of the compiler from that quote.
We can't guarantee that the implementation is correct without writing a full-on certified compiler, but we're working on a theoretical proof of correctness of the type system.
Issues relating to compiler correctness do come up in the real world, and occasionally they lead to vulnerabilities. However, such issues are much rarer than issues stemming from undefined behavior documented as such in the C/C++ standards. So we're more focused on eliminating undefined behavior from the Rust language at the moment than proving the Rust implementation correct.
> issues stemming from undefined behavior documented as such in the C/C++ standards. So we're more focused on eliminating undefined behavior from the Rust language at the moment than proving the Rust implementation correct.
That's exactly the problem. Since C and C++ specifications have UB, compiler writers could anything they feel right.
When I say spec I mean the language specification itself. If we are on the same page on this, then yes, I agree that the spec should be proven correct. If not, please excuse my lack of knowledge in compiler and language construction.