3 ms·
Changing C to have less extensive UB doesn't give you correctness. It gives you slightly less wrong code with possibly slightly different performance properties
by JonChesterfield 3y ago
Changing C to have less extensive UB doesn't give you correctness. It gives you slightly less wrong code with possibly slightly different performance properties.
Correct code looks something like write the thing in a theorem prover, where it mostly suffers existentially.
So give you can't/won't write correct code, all you have is a Pareto surface denoted by performance and correctness aspects, and the distance between what you're shipping and that bounding optimum.
- gavinhoward 3y agoAuthor here. While you are technically correct, the key is your own statement: > where it mostly suffers existentially. Yes, theorem provers exist, and they work. But proving that the end result, the actual machine code, corresponds to the proven code, is the big problem. When I talk about correctness in the post, I'm really referring to two things: 1. Correctness as you have defined it, 2. The compiler artifact being as faithful as possible to the input source code. Avoiding UB is an excellent way to improve the latter.