I'm a huge fan of Rust, but I was under the impression that the domains where Ada is most commonly used are very risk-averse, so I presume Rust is still a bit young for a lot of the Ada use cases.

I agree. Ada has been around and picked apart for high-integrity software jobs. I am personally learning SPARK2014, the subset of Ada. It has formal verification as part of the toolset. I would think Rust would need to develop similar formal tools and not just the PL to be used in the same industries as Ada/SPARK2014. I know somebody is going to link to the use of Rust for something in aerospace. I know Julia is touting something to do with air traffic control, but the core of these high-integrity applications need the full gamut of design tools around the PL. I still like Rust, but I am also playing with Zig.

> It has formal verification as part of the toolset. I would think Rust would need to develop similar formal tools and not just the PL to be used in the same industries as Ada/SPARK2014.

There are people agreeing with you, and they are trying to make it happen: https://ferrous-systems.com/blog/sealed-rust-the-plan/

Thank you. I hadn't heard of it before. I would like to see it happen. I do think it will take many man-years to catch up with Ada/SPARK2014 and win industry favor and confidence, but it's good to see.

Ignoring that the engineering sphere that generally uses Ada works on multi-decade timelines, making Rust a bit too young and immature...

Ada and Rust don't have 1:1 comparison on their safety guarantees.

Rust makes a lot of guarantees around memory safety that Ada does not, whilst Ada is far more focused on correctness. Whilst related, these are very different.

what correctness does ADA focus on ?

SPARK is a formal proving system for Ada. Formal correctness is what they focus on, that Ada can safely prove mathematically how a function will behave, and how a body of functions will behave.

If you're using Ada without SPARK, it will try and enforce these same guarantees, but generally with a runtime contract system, rather than compile time.

I've always wondered this - Does the compiler actually use all that contract information, or is it just the prover?

As of Ada 2012, the redesign means that the compiler can make use of the contract information, and was one of the main reasons for a lot of the changes.

That makes sense. Otherwise why bother conflating the programing language with the verification language.

pretty nice, is the SPARK market lively ? I'd love to see how work is done there

Lively, but proprietary. A lot of SPARK stuff tends to be automotive, factory designs, fabrication and the sort of stuff where people working there are buried under dozens of NDAs preventing them from discussing their work in any way.

But projects tend to have a longer shelf-life. Contracts expected to take a decade to complete aren't unusual, and the product can be expected to be in use for twice that, or longer.

Would they even have a choice?

Good point