If any Ada users are here, I have question on one section:

  procedure Main is
     type Distance is new Float;
     type Area is new Float;

     D1 : Distance := 2.0;
     D2 : Distance := 3.0;
     A  : Area;
  begin
     D1 := D1 + D2;        -- OK
     D1 := D1 + A;         -- NOT OK: incompatible types for "+" operator
     A  := D1 * D2;        -- NOT OK: incompatible types for ":=" assignment
     A  := Area (D1 * D2); -- OK
  end Main;

> The predefined Ada rules are not perfect; they admit some problematic cases (for example multiplying two Distances yields a Distance) and prohibit some useful cases (for example multiplying two Distances should deliver an Area). These situations can be handled through other mechanisms

I can get why you have to be explicit in type casts if you're trying to be safe, but is there any way to say that

  type Area is Distance * Distance

Or

  Type CubeVolume is Distance * Distance * Distance

So that of I say a: Area and b : CubeVolume and a := d1 * d2 it just works, and then b := a * d3 also works.

IOTW, explicit casts not needed.

Or is it the case that Ada really took the concept of "explicit is better than implicit" and went to town?

I just wonder because I love F#'s unit of measure types and how they can prevent logical type errors (say, multiplying 10 m/s by 3kg when assigning to a variable of type m/s^2).

Or for this case, if I wrote

  x: Distance := y: Distance * z: Distance

It'd fail hard, because a Distance * a Distance is an Area.

I sorta figured Ada would have invented this sorta stuff and then it was cribbed by other languages.

So yeah, wondering what the other mechanisms the author mentions are. Because I've always heard Ada is great at type safety, so I'd be keen to see how safe it makes your code when combining values with units that aren't logical to combine.