High-performance safe software

So called "safe languages" are shit because they are slower than C, so you end up giving away performance. How to avoid this performance-security trade off?

Follow seL4's example.
Verify the software through formal mathematical proof using a theorem prover (such as Agda, Coq, Isabelle, etc.). This will assure that the specification of a piece of software has certain properties and, then, that a design (in C) implements a specification correctly. In recent years, it has become possible to apply formal verification directly to the code that implements the software and to show that this code has specific properties.

In other words, you get a C program (high-performance) that is mathematically shown to have no buffer overflows, null pointer exceptions, use-after-free, or anything else you designed in the theorem prover.

>>31

At some point humans have to make the decisions, not the machines, and there are always going to be idiots to screw things up no matter what

Yes but programming with proofs is an excellent way to improve correctness through redundancy. First you tell the computer what your algorithm is supposed to do, then you actually code the algorithm. Knowing the intension behind your code, the compiler can double-check it and tell you if what you wrote is not exactly what you wanted. Without that proof-of-intension, the compiler has no idea what you're trying to do and so will blindly execute every instruction no matter how erroneous it is.