1. So does Python which is quickly becoming one of the most commonly used programming languages. Why? Because it's the defacto standard for machine learning. You see in the real world programming languages thrive because of the ecosystems they power, not because of syntactic details.
2-3. Not entirely sure what you mean but see point 1. 4. Many of Ada's type annotations are avalaible for Nim and eventually we'll have a proof engine that enforces `requires` and `ensures` annotations. Don't hold your breath though. But then I don't see too many people moving to Ada just because it has these. To be honest Ada lost against Rust anyway afaict.
