>'Safe' programming languages will improve security, presumably at the cost of usability through decreased performance. A bit like how a Ferrari is faster than a Volvo, but not as safe.
This is fundamentally untrue. Safeness of the kind described in the article does not come at the cost of performance -- all type checks, invariant conditions and general formal proofs of correctness are determined at compile time. The produced code is to be indistinguishable from a correctly written, efficient C program. You are allowed to play as much as you like with direct memory accesses and use all the dirty tricks you like as longs as you can prove that the resulting program is formally correct.
What could be argued is that price you pay for all this is the difficulty of writing such programs. But definitely not their performance.
Ok, point taken, if you take the pre-processor or code generator approach such as in the article the performance hit might be manageable, but when I look at that 'memcpy' example I can't help but suspect that that is not a free lunch (as in, that all the extra work is done at compile time). For that you'd need to look at the code generated.
Even if there is a 0 performance hit in this case, the majority of 'safe' languages are neither pre-processors for C or code generators for a C like language (which would presumably also require the linked libraries to be re-written using something safer).
So in the specific case outlined here this may be true but in the more general case there are usually run-time trade-offs involved.
I think the key operative word in your comment is 'correctly', writing correct C is extremely hard and this approach makes it harder to create a certain class of bugs at the expense of making it harder to write the program in the first place. Tough choice, even in the absence of a performance hit!
In the example given in the article there are no run time costs. The generated C code is much the same as the original C code from OpenSSL. There is no ATS runtime that gets included either.
This is fundamentally untrue. Safeness of the kind described in the article does not come at the cost of performance -- all type checks, invariant conditions and general formal proofs of correctness are determined at compile time. The produced code is to be indistinguishable from a correctly written, efficient C program. You are allowed to play as much as you like with direct memory accesses and use all the dirty tricks you like as longs as you can prove that the resulting program is formally correct.
What could be argued is that price you pay for all this is the difficulty of writing such programs. But definitely not their performance.