1: Perhaps, but I often know via information not available to the compiler (it might be to a SPARK proof) that overflow won't happen and I don't want to check for it.

2: Programmers can't be trusted to do this kind of free-form reasoning correctly, as attested by the unending stream of security vulnerabilities arising from undefined behaviour in C and C++ codebases.

The push for safe languages is motivated by pragmatism, not theoretical purity.