Rust's safety guarantees are also undecidable on an arbitrary program, but Rust still proves them for safe rust code. Why so? Because safe rust code is not an arbitrary program, it is specifically forbidden from doing some things, which becomes a pain in the ass sometimes for a coder, but the result is a subset of programs you can prove safety guarantees for.

The issue is how to design a language that restricts programmers in a way you can prove everything you care for on their programs, and still don't make life of programmers unbearably difficult, because the language allows them nothing.