Thanks for sharing the video. "Solving the wrong problem" is indeed a persistent challenge and a well-recognized pitfall in engineering. Ada/SPARK offered capabilities before Rust that remain unmatched today. SPARK provides machine-checked formal verification that proves absence of runtime errors, bounds violations, and functional correctness at compile time—not just memory safety. In contrast, Rust's verification tools are experimental research projects retrofitted onto a language designed for different goals.