One thing that document doesn't mention is alire, which is a rather complete tooling. If you want to try out ada, check out https://docs.adacore.com/live/wave/alire/html/alire/index.ht...
I also learned a bit of SPARK, and there the situation is much worse. The Adacore link shows less than the bare minimum: I couldn't get my simple programs (AoC) to the "silver" level, where it passes all checks, let alone "gold", where you actually prove correctness. The rest of the internet is practically barren when you search for SPARK. I got a second-hand copy of Building High Integrity Applications with SPARK; John W. McCormick, Peter C. Chapin. It contains complete examples, and explains the concepts pretty much in depth. Unfortunately, the book is expensive, and since I was just dabbling, I got the cheapest, which was the 2015 edition, which lacks later changes.
There's an Ada forum (https://forum.ada-lang.io/), but it is not very active, and questions may not be answered.
I should give Ada a try and build something fun with both of them
It'd be great to hear from anyone who is using it today by choice.
I like it better than C and C++ and the compiler is included in Debian in a reasonably recent version that it can compile the code that I need.
Ada is particularly nice for programming RPI 2040 microcontrollers because for my needs I didn't need additional libraries. For both of my RPI 2040 projects (one of which is online here: https://masysma.net/37/dcf77_vfd_raspi_clock.xhtml), my code had fewer bugs than I had anticipated.
For general purpose systems programming the lack of free software libraries is still a concern e.g. while working on a custom backup restore program I had to write my own LZ4 extractor and Blake3 hash function implementation because there wasn't any existing libraries that I could find for the purpose.
That's probably why you don't find LZ4 and Blake3 libraries. You forgot to look for the C libraries, which many Ada users would use.
https://www.wevolver.com/article/nvidia-adoption-of-spark-us...
https://www.rocketsoftware.com/en-us/products/cobol/visual-c...
Latest standard is from 2023.
Nowadays everyone is moving into natural language programming, writing even longer prompts than COBOL applications.
I can provide the list, in case you don't find it from previous comments.
Also NVidia rather use Ada/SPARK instead of Rust for their automotive systems.
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.
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.
Tool-wise - refactoring was a bit of a pain.
Could you share what tools you were using, and what you felt was missing? I write Ada in vscode, because it's what I use in my dayjob. AdaCore's plugin has good language support^1, but I don't use it for much other than formatting, or expect sophisticated automated refactoring functionality from it.
^1: It's still missing support for some Ada202x features. I can't wait for it to support `return when...`.