There was a discussion here a few years ago ( https://news.ycombinator.com/item?id=2686580 ) about memory vulnerabilities in C. Some people tried to argue back then that various protections offered by modern OSs and runtimes, such as address space randomization, and the availability of tools like Valgrind for finding memory access bugs, mitigates this. I really recommend re-reading that discussion. My opinion, then a…
Speaking of proofs, how about we write security critical code in haskell? You need a very simple runtime, but beyond that it would work pretty much wherever. Most memory-related bugs are automatically eliminated, and security proofs are easier.
It's a crypto DSL that I believe is implemented in Haskell (it compiles to Haskell, C, C++ and a few others).