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.

>>12

The only trade-off: time spent on the project.

Well there you go, as we all know, all programmers have all the time we need to formally prove C code because the binary code is faster oh wait... no, we don't have all that time. We use safe languages because programmer time is more expensive than computer time, it's quicker to deliver software using safe languages. We will use C when it's obvious that we need a strict account for the computer resources we need. The vast majority of application programming on high-powered general-purpose computers do not have such a requirement.