> I just wonder if our time would be better spent developing tools to formally verify memory safety of existing languages, instead of trying to "rewrite everyth

> I just wonder if our time would be better spent developing tools to formally verify memory safety of existing languages, instead of trying to "rewrite everything in Rust" to get safety. In theory, that makes sense. Now, as a sibling post points out, such tools have been around for dozens of years. Microsoft started using these tools for drivers around the time of Windows XP, if I recall correctly. I've used such tools. Heck, I've developed such tools. In my experience, they require orders of magnitude more experience (both of the tools, of the underlying theory and of the codebase) than Rust (or Ada, or other safe languages) to achieve comparable levels of safety.