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.

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.

And how do you prove that the specification is correct, or that the "certain properties" are what you want anyway? What, or who, defines those? Are the requirements correct or wanted? Does this software do what the users really want? Does it not oppress the users? ...? ...? What is the meaning of life?

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, so why don't we stop creating more abstract bullshite that just takes freedom and responsibility away from humans and encourages them to be even more stupid, teach people to think correctly, and take the idiots out back to be shot!