The thing is, one can write memory safe code in C. The problem is the difficulty in verifying it is memory safe.
I've opined before that this is why, soon, people will demand that internet facing code be developed with a memory safe language.
The thing is, one can write memory safe code in C. The problem is the difficulty in verifying it is memory safe.
I've opined before that this is why, soon, people will demand that internet facing code be developed with a memory safe language.
One can generate safe C code. We have ample evidence that a human being can't sit down and write it.
EDIT: typos
The Core Guidelines have been in development for a long time now; and they do only catch a subset of issues. I'm all in favor of making languages safer overall though!
For applications that demand both maximum speed as well as maximum security, the best solution is probably something like a C compiler that requires the code to be accompanied by formal proofs of defined behavior. Even this will necessarily sacrifice speed in a theoretical sense, because there are certain problems for which the fastest solution is safe but can't be proven safe within (PA/ZF/ZFC/insert any consistent foundation of mathematics you like).
Eventually we'll have people writing fast programs and proving their soundness using large cardinal axioms which might or might not actually be true. Then someday one of those large cardinal axioms will turn out to be inconsistent [1] and suddenly some "proven" code will be proven no more.
[1] https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theore...
A contrived example: there are certain large cardinal axioms that imply the consistency of ZFC. Thus ZFC cannot prove those axioms unless ZFC is inconsistent (Godel's incompleteness theorem). Consider the following problem: "If ZFC can prove 1=0 in n steps, output 1. Else, output 0." A naive solution would brute-force search all ZFC-proofs of length n. A faster solution would be: "Ignore n and immediately output 0." This is correct, because ZFC never proves 1=0. You could formally verify the correctness by using certain large cardinal axioms, but not using raw ZFC.