2 ms·

A well-formed C++ program is one that is "[...] constructed according to the syntax and semantic rules" (4.65). And of course adherence to many semantic rules

A well-formed C++ program is one that is "[...] constructed according to the syntax and semantic rules" (4.65). And of course adherence to many semantic rules in C++ cannot generally be verified statically: "A conforming implementation executing a well-formed program shall produce the same observable behavior as one of the possible executions of the corresponding instance of the abstract machine with the same program and the same input. However, if any such execution contains an undefined operation, this document places no requirement on the implementation executing that program with that input (not even with regard to operations preceding the first undefined operation)." (4.1.2.5). It sucks but that's the way C++ work, and it would be hard for it to be any other way without GC or going full rust.

tialaramex 3y ago
> A well-formed C++ program is one that is "[...] constructed according to the syntax and semantic rules" (4.65). Yes, my argument is that as a result a C++ program which sorts floats in the standard way is not well-formed. The type "float" matches the syntax rules, but does not match the (unchecked) semantic rules for ordering. This is Ill-Formed No Diagnostic Required, IFNDR. Not checking is a choice. You mentioned "full Rust" as the alternative here, but lest that be misinterpreted, the other choice isn't to do everything Rust does, only to make the same choice in this specific respect: Rust chooses to reject programs unless it can see that they meet the semantic rules, while C++ chooses to accept programs unless it can see why they cannot. Rice's Theorem forbids the obviously ideal outcome (accept exactly the set of programs which have the desired semantic properties) but either of these alternatives delivers an implementable system, and I believe of those two options one is clearly unacceptable.
- gpderetta 3y ago
  > my argument is that as a result a C++ program which sorts floats in the standard way is not well-formed. I think the argument is flawed: if any program that sorts floats is not well-formed because a float could be a NaN, then any program that dereferences a pointer is not well-formed as a pointer could potentially be null. Do you agree that's obviously not what's intended? I will grant you that the standard is very much less than clear, but I think generically it uses the term "program" to refer to programs, part of programs or execution of programs. re: full rust, yes I meant "reject programs unless it can see that they meet the semantic rules".
  - tialaramex 3y ago
    I agree that dereferencing a nullptr is merely UB and your program isn't Ill-Formed as a result. I distinguish sort because it requires the sorted type to match a bunch of concepts and those are defined such that if your type doesn't match the syntax requirements it just won't compile, but if your type doesn't match the semantic requirements (the "model" of the concept), which are just text in the standards document, well, too bad IFNDR. I think you can attempt to read the Concepts wording as if it's not about types but groups of runtime values, but I think that gets to the causality problem, where we're deciding at runtime whether our program's text was ill formed before it was compiled. Obviously C++ 17 sort didn't do any of this, because C++ 20 Concepts didn't get standardised until C++ 20 -- hence my reference to "C++ today". I believe in C++ 17 similar code just has UB. Edited to add Also: Unrelated to our main topic, I think C++ 17 should have insisted on a Quality of Implementation requirement here which says yeah, if you gave us faulty comparison function, your data does not get "sorted" whatever that could mean, but we're not going to give you Undefined Behaviour. After all C++ did eventually forbid naive Quicksort, which is a QoI decision. Rust can cheerfully "sort" a bunch of my misfortunate::Always types, which insist they exhibit Total Order but are lying. Obviously after we've "sorted" them they're not "sorted" because that's meaningless, but Rust isn't going to run off the end of a buffer or cause other nonsense, we broke it => we bought it, no more than that.

tialaramex 3y ago

> A well-formed C++ program is one that is "[...] constructed according to the syntax and semantic rules" (4.65). Yes, my argument is that as a result a C++ program which sorts floats in the standard way is not well-formed. The type "float" matches the syntax rules, but does not match the (unchecked) semantic rules for ordering. This is Ill-Formed No Diagnostic Required, IFNDR. Not checking is a choice. You mentioned "full Rust" as the alternative here, but lest that be misinterpreted, the other choice isn't to do everything Rust does, only to make the same choice in this specific respect: Rust chooses to reject programs unless it can see that they meet the semantic rules, while C++ chooses to accept programs unless it can see why they cannot. Rice's Theorem forbids the obviously ideal outcome (accept exactly the set of programs which have the desired semantic properties) but either of these alternatives delivers an implementable system, and I believe of those two options one is clearly unacceptable.

gpderetta 3y ago
> my argument is that as a result a C++ program which sorts floats in the standard way is not well-formed. I think the argument is flawed: if any program that sorts floats is not well-formed because a float could be a NaN, then any program that dereferences a pointer is not well-formed as a pointer could potentially be null. Do you agree that's obviously not what's intended? I will grant you that the standard is very much less than clear, but I think generically it uses the term "program" to refer to programs, part of programs or execution of programs. re: full rust, yes I meant "reject programs unless it can see that they meet the semantic rules".
- tialaramex 3y ago
  I agree that dereferencing a nullptr is merely UB and your program isn't Ill-Formed as a result. I distinguish sort because it requires the sorted type to match a bunch of concepts and those are defined such that if your type doesn't match the syntax requirements it just won't compile, but if your type doesn't match the semantic requirements (the "model" of the concept), which are just text in the standards document, well, too bad IFNDR. I think you can attempt to read the Concepts wording as if it's not about types but groups of runtime values, but I think that gets to the causality problem, where we're deciding at runtime whether our program's text was ill formed before it was compiled. Obviously C++ 17 sort didn't do any of this, because C++ 20 Concepts didn't get standardised until C++ 20 -- hence my reference to "C++ today". I believe in C++ 17 similar code just has UB. Edited to add Also: Unrelated to our main topic, I think C++ 17 should have insisted on a Quality of Implementation requirement here which says yeah, if you gave us faulty comparison function, your data does not get "sorted" whatever that could mean, but we're not going to give you Undefined Behaviour. After all C++ did eventually forbid naive Quicksort, which is a QoI decision. Rust can cheerfully "sort" a bunch of my misfortunate::Always types, which insist they exhibit Total Order but are lying. Obviously after we've "sorted" them they're not "sorted" because that's meaningless, but Rust isn't going to run off the end of a buffer or cause other nonsense, we broke it => we bought it, no more than that.