I understand, the Indices type is defined so it can (optionally and/or later) be re-defined for different platforms. And we have then one place to do so.

As for restrictions, I get it (and re-reading the GNAT documentation with your explaination in mind, makes it clear)

Yours,

-A.

On certain platforms, we would want Indices to be, e.g., a 16-bit word, rather than a 32-bit Natural; and at any rate on ~no~ platform do you actually ~require~ a full "maxint" range for indexing arrays of Word (think about it.) The formulation given in Ch. 1 makes for a clear type hierarchy. (Really, anywhere you see "Natural" is simply a placeholder for a narrowly machine-specific type, if such were available.)

> I only find them hard to "fit in head"

The clearest, IMHO, way to think about this: the restrictions, properly speaking, are not part of the program; they are statements ~about~ the program, which certain compilers are able to mechanically verify.

To put it another way: the behaviour of the program should not change upon a removal of any or all of the restrictions, supposing that the compiler (e.g. my copy of GNAT) on which the same program was able to build ~with~ the restrictions is not buggy/malicious and did not lie regarding having enforced them upon that successful build.

As for: "Do we need Word_Index or Indices?". I'm all for constraining a type, so defining a custom (and different) index type for words and bits etc. But why not derive these directly from Natural and have an extra Indices. (BTW It is only a small point)

As for: "Are we lucky this is correct?", I'm sorry this comes over as an accusation that it was not worked out in detail by you (I've followed the development, and know and appreciate your thoroughness!). I hoped to motivate the reader to work this out in head or on paper. My original analysis of the Carry / Borrow code did not take into account an extra possible carry from an earlier summation / subtraction.

As for the restrictions: I like the use of as many restrictions as possible (creating a list of the restrictions that were not used was mainly an exercise to understand the list itself). I only find them hard to "fit in head" (consequences including).

Yours,

-A.

Re: the restrictions: aside from the "No_Recursion" item (prohibited on account of Karatsuba), the bulk of the unused ones were simply not present in my particular GNAT. (Every GNAT I've used, barfs on encounter with any restriction it doesn't know about; try it yourself.)

"No_Exception_Handlers" and "No_Exceptions" are absent for the obvious reason. Ditto re: "No_Long_Long_Integers".

Theoretically 2017 GNAT ought to work, but you will have to fiddle with the Restrictions.
The general idea is to build under the tightest possible (but not tighter... see above) set of Restrictions for any particular GNAT.