I'm also not sure what your disagreeing with exactly. The reason all those assistive tools for C exist is because C is popular for orthogonal reasons, but also its undefined behavior is known to be a source of danger & uncertainty. That's why compilers undergo qualification for instance. The undefined behavior is characterized, catalogued, and codified to turn it into de facto defined behavior.
No, this is not true. Again, the fact that a[i] is undefined for values of i greater than or equal to the array's length does not necessarily make guarantees about the value of a[i] more difficult when it is defined, and it certainly does not impact the soundness in that case. Verification methods can -- and do -- deal with undefinedness without making it "de facto defined". Indeed, even in arithmetics 1/0 is not defined, and yet Peano arithmetics is fine. Formal logic in general does not require every expression to be defined (in the sense of having a certain specific value) in order for it to be sound.
I agree that undefined behavior is a problem, but it is not necessarily worse than other problems when correctness is concerned, and it is not true that it affects the soundness of inferences. It can certainly be tricky or confusing, though, and it is certainly a source of incompatibilities, which is why most languages try to avoid it or control it (Rust has undefined behavior inside unsafe, and Zig can dis/allow it depending on compilation level).
A whole bunch of the tests and the developer interface agreement that come with your purchase of a IEC/ISO qualified C compiler are around establishing what that instance of the compiler does with undefined behavior corners of C. The whole point is to have evidence of turning unknowns into knowns for a defined set of deployment constraints.
> Again, the fact that a[i] is undefined for values of i greater than or equal to the array's length does not necessarily make guarantees about the value of a[i] more difficult than if it were defined, and it certainly does not impact the soundness in cases where i is within bounds.
That's because you know the surface area of what's defined and what isn't already. If the behavior for a[i] were undefined for all cases of a[i], then you wouldn't be using a[i] at all because you'd have no idea what to expect about its behavior.
> I agree that undefined behavior is a problem, but it is not necessarily "worse" than other problems
You seem to be making this argument on the basis of taking for granted that you know something about what is defined already. Here's how to know that undefined behavior is worse. Say I asked you to write a program for your own pacemaker in a language where _all behavior_ is undefined. What do you do? It will be impossible to avoid killing yourself except entirely by accident, unless you resort to external validation methods.
The assurances that are possible in things you're describing are predicated on having some known a priori model for the domain of what is defined and what isn't, and the various certification/qualification methods required to use certain technologies & tools in domains where these things tend to matter focus on keeping engineers inside the bounds of what's defined and reducing the scope of what is undefined for a given configuration in-use.
Maybe, but undefined behavior still doesn't kill soundness.
> That's because you know the surface area of what's defined and what isn't already.
Sure, but in every programming language most of what you do is defined, even in C.
> Say I asked you to write a program for your own pacemaker in a language where _all behavior_ is undefined. What do you do? It will be impossible to avoid killing yourself except entirely by accident, unless you resort to external validation methods.
It's impossible to write any program in a language where all behavior is undefined. Such a language, by definition, has no semantics, and so no notion of a program. In fact, a language with no semantics of any kind is not a language at all.
> The assurances that are possible in things you're describing are predicated on having some known a priori model for the domain of what is defined and what isn't,
This is true for all programming languages.
So, it's necessary to remove a sufficient amount of undefined behavior before something is even usable in a coherent way? Which is another way of saying, you have to have defined enough behavior to be able to even get to the point of knowing whether or not the programmer is the one responsible for the "bug".
Undefined behavior seems to be necessarily worse than programmer error, since to be able to determine the latter you have to have removed some part of the former.
:shrug:, going to get back to work.
It's like asking which is "worse", saying "England is a country in Africa" (false) or "Love ate a circle" (meaningless)? Both are "bad" in their own way.
But undefined behavior can certainly be inconvenient, because it is insufficient to determine whether a sentence is "well-formed", i.e. grammatically correct, in order for it to be meaningful, as some grammatically correct sentences are nonsensical. But it's certainly not catastrophic, because mathematics has a lot of undefined sentences, and we still use it successfully.
I.e. the mere existence of undefined behavior in the formal system does not negate the soundness of the entire system. At least it doesn't in arithmetic and it doesn't in C. In fact, C is currently the language with the best formal verification tools. Of course, that is out of necessity, but it's absolutely false that the presence of undefined behavior in the language breaks the possibility of sound formal deductions.
It is true that C does make some local logical inferences more tedious, and some of that is due to undefined behavior, but that's a whole other discussion.
[1]: Deductive proofs are very rarely used in real safety critical system, and they're especially unpopular even compared to other formal methods such as sound static analysis and model checking. Those two are more commonly used in safety critical systems, but the most common assurance tool is tests.