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.

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.

There a two stacks, the call stack, and a stack for returned values of dynamic size, not very complicated, is it?

Yes that is what I mean by allocation being handled by the compiler.

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

Accesses - pointers - are automatically nulled when declared. So you won't silently screw up who-knows-what with an uninitialized access, though yeah, it's not perfectly safe.

You can also declare access types as "not null" in which case initialization is compulsory.

http://www.ada-auth.org/standards/12rm/html/RM-3-10.html#p13...

I didn't mean pointers/access-types, I meant ordinary integer-type locals.

You can put a pragma Warning_As_Error ("never assigned"); or the respective compiler switch on GNAT.

Other compilers have similar switch.

Heck even C and C++ have them, although few make use of them.

Also, I think Ada is fully memory-safe but for initialization. That is to say, the only way in which it's not memory-safe, is regarding uninitialized variables. (That's assuming of course that you don't disable checks.)

I'm not sure if it lets you shoot yourself in the foot regarding invalid type conversions, misuse of unions, that kind of thing.

Pragma Initialize_scalars for the win. But at runtime.

And if you can afford it, Codepeer (static analysis) finds most of the ones the compiler doesn't find. And then if you can live with the Spark subset, you get proof of initialization in 'bronze' mode :-).

In addition to what other's have mentioned in direct response to the examples you mentioned, there are additional safety factors - both by default and opt-in.

Pointers - accesses in Ada parlance - have rules that help ensure you can't have an invalid access. For one, the object itself has to be declared 'aliased' to create accesses to it. There are also rules to do things like ensure you can't create an access to some type at a higher scope than the type itself.

There are also memory pools that you can use. So you can specify that all allocations of a type occur in a specific pool or sub-pool. In addition to letting you control how allocation occurs, you can also use them for memory safety. All items in a sub-pool will be freed when the pool falls out of scope, so you can simply leave deallocations to occur that way.

There are also concurrency tools baked-in, with runtime support at least. Specifically in terms of memory safety, you have protected objects. They will automatically ensure you have a single writer at a time, and will do other nice things like still allow multiple readers. If you need to, you can get a fair bit of control over how it all works.

From the book:

> dynamic checks (such as array bounds checks) provide verification that could not be done at compile time. Dynamic checks are performed at runtime, similar to what is done in Java.

Check out the table on https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce....

> SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.