Ada for the C++ and Java Developer [pdf]

Also available as HTML:

https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...

Yes they are bounds checked, at compile time, or runtime if not able to prove them at compile time.

Overflow is checked.

However both can be disabled via unsafe code pragmas if so desired.

As of Ada 2012, the SPARK proof system was integrated into Ada and you can also use DbC as formal proofs.

Many of the use cases that in C++ would require new/delete are handled by the compiler itself, thus there is an error if when a function is called there is not enough space available.

In the cases that there is a need to explicilty do malloc/free like programming, only malloc (new) is considered safe, manually releasing memory is an explict unsafe operation and marked as such.

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.

In addition Ada allows dynamically-sized arrays to be allocated on the stack and to be returned from a function. Efficient implement of the latter requires rather non-trivial support on the compiler side and C/C++/Rust have nothing like that. Yet in many cases it allows to eliminate new/delete and simplify code.

For example, just consider if C allowed to return a plain C string from a function without any heap allocation. Things like unsafe sprintf/strcopy would never happen then.

Although Ada still isn't fully memory safe. Read-before-write causes undefined behaviour, if I recall correctly.