I've used it in my personal hobby projects for several years now, Ada/SPARK is a favourite language of mine. It's not a legacy language and it has features which I wish mainstream languages would have, particularly regarding the formal verification utilities of SPARK. It's also great for bare metal development.
I've not managed to convince anyone else to use it, as most are discouraged by either its Pascal-style "verbose" syntax on first glance or its general lack of third-party libraries (relative to something like Rust's ecosystem). Anyone who can get past those aspects should really give it a try.
The abstract syntax of Ada is in many cases superior to that of the C-derived languages, but I also dislike its verbosity.
At least for personal projects, the verbosity can easily be avoided by using a preprocessor for the Ada source files. This is what I do.
Unfortunately, this would seldom be considered acceptable in a business context, because the non-standard appearance of the language would be considered an obstacle for developers unfamiliar with it, so it would complicate the future maintenance of a project.
It would have been nice if one of the revisions of the Ada language would have provided a standard set of abbreviations, e.g. for using various kinds of Unicode bracket symbols instead of the keywords currently used for this purpose.
There would have been nothing unusual in this. In the past many programming languages have defined alternative representations for the tokens, both a verbose representation and an abbreviated representation that may use more symbols, for instance PL/I and ALGOL 68.
I've not managed to convince anyone else to use it, as most are discouraged by either its Pascal-style "verbose" syntax on first glance or its general lack of third-party libraries (relative to something like Rust's ecosystem). Anyone who can get past those aspects should really give it a try.