[ajdude]

Ada is memory safe if you just work with the stack or avoid Unchecked_Deallocation. Since functions can allocate and return entire arrays and other data structures completely on the stack, you don't need to mess with the heap that often (and when you do, you can also define your own memory pools).

If you have to use dynamic allocation, you could also use the built in container libraries or controlled types for additional safety.

Though if you want the kind of memory safety that Rust has, there's always SPARK (a subset of Ada).

[bluGill]

Is there a free version of SPARK? Proven correct code appeals to me, but I don't enjoy trying to get anything past purchasing.

[ajdude]

SPARK is free by default, and readily available. You can use it as-is in ada by adding " with SPARK_Mode => On" to your code; here's some examples: https://learn.adacore.com/courses/intro-to-spark/chapters/01...

You can install gnatprove with alire via "alr install gnatprove"

[mcguire]

It's been a while since I looked at SPARK and Ada, but the last time I did, SPARK was very well integrated with the GNAT Studio IDE.

I still preferred frama-c, because C, but it's a really nice toolchain.

[kevlar700]

Ada goes beyond memory safety.