10 ms·
So IFNDR is a property of programs, whereas UB is a property of executions of programs. Got it, thanks. Given that IFNDR is a static, rather than a dynamic pro
by School-Cotton 3y ago
So IFNDR is a property of programs, whereas UB is a property of executions of programs. Got it, thanks.
Given that IFNDR is a static, rather than a dynamic property, why can't compilers detect it and error? Are all IFNDR issues similar to the ODR one you mentioned in that they only arise at link time and fixing them would require changing how symbols are mangled?
- tialaramex 3y ago> Are all IFNDR issues similar to the ODR one you mentioned in that they only arise at link time and fixing them would require changing how symbols are mangled? No, they're worse. Are you comfortable with basic CS theory? If not this is likely to whizz over your head, sorry. A typical IFNDR issue depends upon the semantic properties of the alleged C++ program. Rice's Theorem tells us that all non-trivial semantic properties are Undecidable. No algorithm can exist to determine whether a program has these properties except if trivially all the programs in your language have the property (e.g. imagine a toy language with no jumping or iterating features, it must halt) or none do (e.g. imagine a resolutely single threaded language, it doesn't have any data races). Because it's Undecidable, having the compiler decide if your alleged C++ program has the desired properties and if not report an error is intractable. So the C++ standard just says if it doesn't have that property it's actually not a C++ program, too bad, the compiler shouldn't worry about this case at all, just press on. Now, the good news about Rice's Theorem is that we do have another option. When we're not sure if the semantic property we wanted is present, we reject the program, with a diagnostic informing the programmer that we couldn't prove it had this desirable property. I'd argue this approach is much better, but it does mean you can write programs in Rust (which has this behaviour) where even though you are totally correct that the program would actually be OK the compiler rejects your program because it can't see why you're right.