And yet, the Rust we have today (which is a completely different language than what Hoare originally intended, long before its 1.0 form), requires a complete redesign and rewrite of a system written in C++. The "rewrite everything" dogma and the extreme complexity of the borrow checker were not part of Hoare's original language.

> but D without a GC is very limited

Why? It's pretty much the same object model as C++, and actually was D indeed designed to be a better C++ and a better C, even by an expert who had many years of experience in writing a commercial C++ compiler. There is no need for a GC if you migrate C++ code; you can still do manual memory management and incrementally switch to GC. Unlike Rust, which requires complex binding generators (like cxx or bindgen) to talk to C++, D has native C++ interoperability built into the compiler, so it indeed supports incremental migration.

> Ada without SPARK is not as safe nor as ergonomic, and Ada with SPARK is very difficult to scale to larger projects.

SPARK is usually used for the safety critical parts of a system, not a whole system. It is a subset of and more limited than Ada. But Ada by itself is already much safer than C++, because you can capture the semantics of a system much closer due to the more precise language features. It also has features which help to avoid dynamic allocations, bounds issues, etc. And even Ada is semantically closer to C++ than Rust.