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.

Someone should write a program that can check any arbitrary program to make sure that it is correct.

Someone should write a program that can check any arbitrary anus to make sure it is anus.

>>41
check_correct () {
grep -q "Rob Pike" $1 && echo correct || echo incorrect
}

>>42
check_anus () {
grep -q "Rob Pike" $1 && echo anus || echo vaginabuttsex
}

>>43
check_manliness () {
grep -q "Ted Nugent" $1 && echo man || echo woman
}

>>44
You are confused. I hope that doesn't happen often when Ted Nugent is involved, but back to the topic at hand. The "manliness" code test is Knuth's “Man or Boy Test”—http://rosettacode.org/wiki/Man_or_boy_test

Actually, I would like to see the Symta solution to this problem.

>>45
Don't you argue with my dbus-4.4, boy.

>>46'
>boy
racist opinion discarded

>>47
Optimize you are quotes.
Until then, your opinions are discarded.

>>48'
>inconsistent grammar
opinion retarded

>>49
Optimize you are quotes. I repeat: optimize you are quotes.

>>50
You keep saying that, but you don't seem to know what it means. Besides, quote optimization is broken on this board.