Sure, in return for bending code over backwards to fit rules you get guarantees; but pretending that is anything but a different compromise isn't helping. If Ada was all that, everyone would be using it; and that's not going to happen, because it's not a realistic approach to programming.
The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place.
I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.
Argument for popularity = superiority. By your same logic, we shouldve stuck with COBOL for important apps since all the big businesses were using it. I have a feeling you dont write new apps in COBOL.
"the complexity of dealing with it will be more or less the same as dealing with the errors in the first place."
The best empirical comparison of C and Ada showed the opposite. All studies showed the safer languages had less defects with usually more productivity due to less rework later on. Evidence is against your claim so far.
"I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety."
Me too. Rust and Nim are taking that approach. People are finding both useful in production so far.
The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place.
I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.