Especially when you add this line, you're telling me that what you want is not to program in C but to program in a language which differs from C not in syntax but in semantics, and in otherwise vaguely undefined terms [1] there. And you're mad that compilers implement C instead of your not-C.
I find claims that you can safely write secure code in C hard to believe when you marry them with complaints about compilers not implementing not-C correctly. Especially given that virtually every new sanitizer and static analysis tool to find issues in C code manages to turn up issues in code that is rigorously tested to make sure it passes every known prior tool (e.g., SQLite).
[1] From prior experience, this tends to be best distilled as "the compiler must read the programmer's mind."
I also don’t believe that a single person on the planet can write a secure c program of meaningful complexity. Static analysis tooling has demonstrated that it isn’t up to the task of saving developers from themselves.
> meaningful complexity
Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....
> It is not possible to remove ub from the spec
did not say "it is not standard to remove ub"...
Not a part of GP's assertion
> and how many people can check the proofs?
it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion:
> Static analysis tooling has demonstrated that it isn’t up to the task
What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter...
In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed?
Are there good examples of what you mean by this? From my own C++ experience, when dealing with c libraries and std::string types, I'll sometimes use the copying api's[0] when passing around std::string::c_str() because I find it easier than worrying about invalidating the returned reference if the string is destructed or modified.
[0]: e.g. https://curl.se/libcurl/c/CURLOPT_COPYPOSTFIELDS.html
I can't imagine why a C compiler would remove a non-trivial runtime check though (except undefined behaviour).
[0] https://wiki.sei.cmu.edu/confluence/display/c/MSC06-C.+Bewar...
If it's too slow, then you probably have an issue with which algorithm/data structure you chose and would have had the same issue in another language.
The biggest issue I have with C today is that you can't trust that your compiler actually generates code that is 1:1 with what you wrote. I'm not talking about UB here, your compiler can actually remove code/checks even though you don't invoke UB.
Then we have UB, I think UB should be removed from the spec completely. There probably was a point in time when leaving stuff as UB was the best option, but today speed is seldom the problem, correctness is.
I no longer work as a C programmer, but I still love the language and I really enjoy writing C code, but I really would like to get rid of UB and have a compiler I can trust to generate code even when I turn on optimizations, and having optimizations off is not an option either, since it can generate broken code as well, so...