Even with your formal methods strawman, vulnerabilities like these are still possible in Linux and C. We need to move on.