I'm curious about this list, because it definitely doesn't seem that way these days. It'd be interesting to see how many of these are still possible now.
I didn't make a list, but let me give an example. Page 22 where variable declarations are introduced:
If a variable is declared and not given an initial value then great care must be taken not to use the undefined value of the variable until one has been properly given to it. If a program does use the undefined value in an uninitialised variable, its behaviour will be unpredictable; the program is said to be erronous.
About two years ago, I was able to dive into the Ada reference manual formatter which has initial commit of March 2000 and is about 45k lines of code, and add MDX output pretty easily.
Other languages focus on terseness and expressiveness. Ada expresses a bunch of constraints directly and forces you to do things in organized ways (e.g. use namespaces appropriately).
The big reason for `out` only is "I want to write here, but I don't care about the initial value." It's a more explicit version of the C++ `Foo& outFoo` output parameter paradigm.
> When "out" and "in out" parameters are distinguished, there is no need for the existence of constructors as a separate concept.
I don't agree with this. You can get I need to do things "post-init" with controlled types, or use a `return X : Thing do ... end return` block. Constructors help ensure invariants. You can make a type `is private` to prevent instantiation, only allowing creation via functions (sort of like Rust `new` associated functions), or initialization via an `out` param. It's OK but not perfect, but you can also tag on a `Type_Invariant` aspect if there are conditions which have to be met by a type. My big problem with Controlled types is that forces a type to be `tagged` (i.e. it has a vtable) which means it affects storage layout of values of that type, which isn't a problem in C++.
You can forbid copies by making something a `limited` type, but you'd have to write your own "Move" equivalent, and some of the containers have `Move` subprograms implemented to transfer contents. Limited types might elide the copy when returned from a function, but it's been a while since I looked at those rules.
I recently started writing Ada again, a couple of years after I did a bunch of projects with it. The amazing things is how easy it is to go back and update old code due to how much semantic information gets embedded in it and how few symbols it uses.
That's because I took it down over two years ago and moved most of the content to ada-lang.io when I set that up. This was an anecdotal blog post so it didn't get moved over.
> the code to SPARK and proving the absence or runtime error
I wrote Rob Pike's simple regex from the "Practice of Programming" in Ada/SPARK and it blew my mind that I actually managed to prove an absence of runtime error (guaranteed no overflow or out of bounds).
What I really like about SPARK is the pragmatism. It's not all or nothing, you can call on non-SPARK code, and you don't have to go full functional verification to profit from the SPARK toolset.
edit: if you feel like sharing your code and experience there, I'm pretty sure some people would be interested.
> you don't have to go full functional verification
The amazing thing to me is that Ada code can call SPARK code just fine, and there's crates of SPARK code in Alire that you can use. It's a huge boost of confidence in the quality of a library that you're using when it has some form of verification.
This is an awesome feature, combined with appropriate type and bounds checking and prevents so many errors. It can also avoid resorting to a heavier-weight map type.
Ada has this as well, including using any arbitrary continuous range for array indexing which handles remapping indices for you. e.g. if the key range is 20-40 the language handles associating it with array indices for you.
I'm curious about this list, because it definitely doesn't seem that way these days. It'd be interesting to see how many of these are still possible now.