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.

>>8
He created ATS just so it was easier for programmers, but it loses performance.

http://cs-people.bu.edu/md/plpv10-danish.pdf

The human resources required for even a relatively small-scale verification are tremendous, as shown by seL4

The seL4 project is based on the family of micro-kernels known as L4 [18]. Recently, a refinement proof was completed [16] that demonstrated the adherence of a high-performance C implementation to a generated executable specification, created from a Haskell prototype, and checked in the Isabelle [21] proof assistant. The Haskell prototype is itself checked against a high-level design. One weakness is that changes made at a high-level can have rippling effects and may require the entire proof to be redone.

If the software you are writing is huge, you have really limited resources and performance isn't an issue, then languages such as ATS may do the job for you.
But there's nothing better than proven-secure C. High-performance and safety. The only trade-off: time spent on the project.