To be fair, I started programming back in 1978 with Commodore PET 2001 and went into C and assembly (6502) after that. I then picked up Pascal. Then J and APL a

To be fair, I started programming back in 1978 with Commodore PET 2001 and went into C and assembly (6502) after that. I then picked up Pascal. Then J and APL after that. While trying Rust for the first time, nailing some of the concepts and syntax (borrow checker, etc.) to express those concepts was very confusing or too verbose to me. Then the second time I tried Rust, I was also learning Zig, and Zig came much easier to me and I could program things quicker albeit without the features of SPARK2014 or Rust for that matter, but a nice sweet spot. But when I saw the goals of Rust and I had already tried SPARK2014, it became apparent that the wish list for Rust was a reality in SPARK2014 and its tooling. The safety, integrity, verifiability, clear and simple syntax along with the formally proven language of SPARK2014, and Ada's legacy seemed the obvious choice to get actual software written for safety-critical applications. I am working on Show Control software which demands high integrity and safety. One leading package, Navigator, runs on QNX. When you are flying things over people's heads at high speeds and accelerations or flying people, you need something that is track proven for such applications. I think Rust can get there someday. I have put Rust on shelf until it matures more on this front. As others have mentioned, Adacore is not so much an PL evangelist as might be thought of by its name, but is cooperating with Ferrous Systems and others to bring Ada/SPARK2014 goodness to Rust. Rust just isn't there yet, and I am a bit too far along to devote my next 10 years to growing and learning Rust when I can apply SPARK2014 today. PL syntax is subjective, and I just find myself tripping over the verbosity in a C++/C-like syntax that Rust adds. I know there are strides to improve this, but