I would say Ada/SPARK gets a lot of things right, too. What it lacks is hype and thus, a vibrant ecosystem. It can be a huge deal-breaker to many people.
I looked specifically at Ada, and for my use case macros are quite important. If I were to use Ada, I would need a separate code gen step.
I also need concurrency without making new threads. I know Ada can do async but it doesn't have something like tokio.
A shame. I wanted to give Ada a try, but didn't get very far before losing hope.