Also add Ada... we tend to forget Ada but it was doing what Rust is before it was cool.

>> we tend to forget Ada but it was doing what Rust is before it was cool.

As someone who has done a fair bit of Rust and Ada programming, this is not quite accurate an overlooks the innovations of Rust and the strengths of Ada:

In my opinion, Rust's biggest innovations are 1) borrow checking and "mutation XOR sharing" built into the language, effectively removing the need for manual memory management or garbage collection, 2) Async/Await in a low-level systems language, and 3) Superb tooling via cargo, clippy, built-in unit tests, and the crates ecosystem (in a systems programming language!) Rust may not have been the first with these features, but it did make them popular together in a way that works amazingly well.

Ada's strengths are its 1) powerful type system (custom integer types, use of any enumerated type as an index, etc.), 2) perfect fit for embedded programming with representation clauses, the real-time systems annex, and the high integrity systems annex, and 3) built-in Design-by-Contract preconditions, postconditions, and invariants. Compared to Rust, Ada feels a bit clunky and the tooling varies greatly from one Ada implementation to another. However, for some work, Ada is the only choice because Rust does not have sufficently qualified toolchains yet. (Hopefully soon . . .)

Both languages have great foreign function interfaces and are relatively easy to use with C compared to some other programming languages. But Ada is not "Rust but from the 1980s" anymore than Rust is "like Ada, but newer".

Having done a fair bit of C programming in the past, today I would always choose Rust over C or C++ when given the choice.

But when working with really big C++ codebases, you don't always get to choose so something like Safe C++ is good to help add Rust-like features to C++ code.

Ada Spark goes beyond safety guarantees of Rust. However how many here want to prove their invariants hold for their UI?

You don’t have to verify your whole application, just set SPARK_Mode => Off where you want to skip it. Alternatively, set the global default to Off and it becomes an opt-in feature.

Proof levels depend on your goals, but most requirements are satisfied by proof of “Absence of Runtime Exceptions” (AoRTE), which is easier than a full formal proof.

How would you prove stuff about your code like memory safety.

Out of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well.

You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html

Even PHP is a perfectly fine, memory-safe language.