If they're really into reducing bugs, they should embed a complete proof system into the language, rather than try to guarantee something as simple as correct memory references - which isn't much of a problem to ensure for anyone serious about the correctness of their code.
Add that if a proof system (that is powerful enough) was available, and people actually used it, the language could do away with the unsafe overrides. It could also be of great help to the compiler to optimize the code, like removing array bounds checks where the programmer has supplied a proof that the index is in range.
Add that if a proof system (that is powerful enough) was available, and people actually used it, the language could do away with the unsafe overrides. It could also be of great help to the compiler to optimize the code, like removing array bounds checks where the programmer has supplied a proof that the index is in range.