I agree with your points except to claify my point on compiler's correctness: > issues stemming from undefined behavior documented as such in the C/C++ standar

I agree with your points except to claify my point on compiler's correctness: > 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.