For my safety-critical automation software for a machine that will operate around people and overhead, I’m choosing Ada/SPARK2014. Its decades-long track record in high-integrity domains like aerospace, defense, and medical systems ensures reliability for applications where human safety is paramount. SPARK2014’s formal verification tools mathematically prove the absence of runtime errors, aligning with standards like DO-178C and ISO 26262, critical for my Q3 2026 market deadline. While Rust is gaining traction for memory safety, its formal verification tools, like LEAN/Aeneas, are still maturing and lack the production-ready ecosystem of Ada/SPARK2014. Ada’s clear, structured syntax simplifies code reviews, and its tooling generates certification reports familiar to regulators, streamlining approval processes. For my project’s safety and business needs, Ada/SPARK2014 is the proven choice - for now. I am not a fan of Rust syntax or complexity, but that is somewhat subjective. I last dove in about 2 years ago.