What ends up happening otherwise in practice, if we go for an axiomatic approach is that the implementation becomes the spec, and there is really nothing (at least not a formal mathematical definition) to judge its correctness against, because you may have mutually incompatible stated properties.
I don't think Rust needs to solve every problem, especially those that cannot be well-specified. It seems more appropriate to provide a solution at the level where guarantees can actually be made (and not just claimed to be made).
I also don't see what's specific to systems programming in the use case here. Why would it e.g. not apply to Haskell but apply to Rust? Moreover, I do not find arguments of the form "A is a systems language, A has X feature. B is a systems language, so therefore it must also have X" persuasive. Ideas need to stand on their own merits, not on whether e.g. C or C++ also do something.
Characterizing languages like C, C++, and Rust as high-level languages is not a new phenomenon. These are general-purpose languages as opposed to domain-specific because... well, just compare Rust to a language tailored for creating music.