I think you're right, but there's very little chance Ada/SPARK will ever become as popular as Rust because of politics. Rust managed, somehow, to get the backing of tech giants like Microsoft and Amazon... the fact it started at Mozilla, a well-regarded company with lots of influence in tech (despite its downwards trajectory in the browser wars) probably means more than any technical advantage Rust has over the competition (though I have to say Rust's type system and the borrow-checker are really inovative on their own and deserve the general praise they receive).

If Ada/SPARK were to be successful, they would need this corporate backing. Maybe that's possible outside the USA? Say, the EU probably has enough influential tech companies and weight to push forward with a Rust competitor that's perhaps superior (as you claim, I don't know enough about SPARK yet to make that claim myself)? I think that would be extremely benefitial to both the tech world AND to Rust and Ada themselves... competition is a great way to make things evolve fast.

EDIT: Ada/SPARK does seem to have a really good advantage over Rust: it's an actual specification, not just a single compiler implementation where "whatever the compiler does" is how the language behaves. This is very important in many industries. I know there's work ongoing to fix this for Rust, but that may take several years and even never amount to anything.