Drumming For Sappeur
"Popular languages in this category don't exist"
That statement is true, but there "exist" languages which are both memory-safe and efficient. You can have most of the efficiency and realtime capabilities of C++ without all the nasty Java properties such as voracious memory consumption and GC freezes. You can have your little command line program start up in less than 10 milliseconds.
More than 50% of all serious exploits in the CVE database are artifacts of the C and C++ languages. Real-world C and C++ programs will have them, because programmers are not superhumans. They don't live in a world of infinite funding and infinite project deadlines. Quite the opposite.
I designed a language called Sappeur and wrote a compiler (or call it a translator if you wish), which assures memory safety. Sappeur is (essentially) a memory-safe subset of C++ and adds some novel support for memory-safe multithreading. The compiler will generate C++ code to be compiled into machine code by GCC or msvc (or potentially any other modern C++ compiler). That took me about 10000 lines of C++ code. I do think the right people could prove correctness of a 10k LOC project, given reasonable time and budget.
But certainly the current version of the compiler will contain bugs. Still, I do think it demonstrates what is possible. It is another line of defence and given that hardware designers are not infallible creatures, we should look for any opportunity to add useful layers into the defence-in-depth armour. Is your MMU proven correct ? If not, will your sandbox ever work as promised ?
Actually, Sappeur programs could *remove* the need for MMUs and consequentially save cost and electric power.