They aren't. Some verification experts and I are: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/pldi117-yang.pdf https://www.microsoft.co

They aren't. Some verification experts and I are: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/pldi117-yang.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... https://news.ycombinator.com/item?id=17051131 https://news.ycombinator.com/item?id=17051131 It's safe if you can prove it's safe. Even C with Frama-C. If the type system can't do it, use an external tool to do it. Tools exist, automated and manual, for doing such safety proofs on high-, low-, assembler-, and microcode-level software. There's a long tradition of verification in hardware, too. Rockwell-Collins even uses the tools common for hardware to verify software and hardware together. http://www.ccis.northeastern.edu/home/pete/acl206/slides/hardin.pdf http://www.ccis.northeastern.edu/home/pete/acl206/slides/har... The real problem, aside from just limited resources to build tooling, is a mindset of trying to rely on one tool for safety instead of mixing up different approaches to get their benefits.