Not an expert in ADA, but after playing around with it for a while, I don't know why this language doesn't get more praise. It seems to solve a lot of the memory problems Rust solves, albeit in a different way. Its first-class arrays and strong type system seem to go a long way into not having to deal with pointers often, for example. These "features" today would likely be considered part of "a better C", except that none of this is even new; ADA dates all the way back to the 80s. And then ADA/Spark allows for formal verification, which C/Rust do not have to my understanding.
Why is ADA not adopted more broadly?