Rust, Zig and Ada code CAN be secure, but most of it is not, it is too easy to write or update Rust, Zig or Ada code so that it is no longer secure or has unexp

Rust, Zig and Ada code CAN be secure, but most of it is not, it is too easy to write or update Rust, Zig or Ada code so that it is no longer secure or has unexpected and unsafe results. The lack of formal verification features and easy-to-stray-into logic errors in Rust, Zig and Ada make it easy to create code that is difficult to fully grasp how it will behave, especially when large projects are concerned. The Rust, Zig and Ada code runs really fast and is usually memory safe but there are hidden dangers lurking. I don't doubt that Rust, Zig and Ada will become more popular in time to come, but formally verifiable languages such as Verifiable C or Spark are actually "safe" in some meaningful sense of the term instead of giving everyone a false sense of "safety" in the form of memory safety features as if memory safety errors were somehow the only class of security critical error.