2 ms·

> Of course, this does assume that a program being well-formed can change between each execution Which can't be right. > has the same causality wackiness, jus

> Of course, this does assume that a program being well-formed can change between each execution Which can't be right. > has the same causality wackiness, just to a far lesser extent than C/C++, in the form of "angelic nondeterminism" It's OK, I don't need to Google, you'll find me in a conversation with Martin Uecker in a previous HN thread about PNVI-ae-udi which is the way C or C++ people would think about the matter. And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on always telling the compiler what's going on, and as a reward we get both more assurance of correctness because the tools work (Miri for example) and better performance. The experiment is about whether most Rust software can live with this restriction ("Strict Provenance") and the answer IMNSHO is clearly yes. Rust's pointers get to have member functions (as do its primitive integers and any other types) and Aria's experiment adds the method with_addr() to pointers, so now we can tell a pointer (which has provenance) that we want a different pointer with a different address inside it (but preserving the provenance) via the method. More pertinently to our discussion, even with PNVI-ae-udi plus a mistake that results in an impossible pointer this is a cause of Undefined Behaviour, which occurs at runtime, it is not a semantic requirement of the language, our Rust program was well formed and correctly translated into machine code if we did this wrong, it's just that it had Undefined Behaviour at runtime as a result of us writing bad unsafe code. Because Rust defaults to rejecting programs it knows always panic there can be the false impression that such programs are not well-formed. You can just insist to the compiler that you want the results anyway, it will duly spit out an executable which... always panics. Not sure what you want that for, but you're welcome to it.

gpderetta 3y ago
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.
LegionMammal978 3y ago
> And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on always telling the compiler what's going on, and as a reward we get both more assurance of correctness because the tools work (Miri for example) and better performance. The experiment is about whether most Rust software can live with this restriction ("Strict Provenance") and the answer IMNSHO is clearly yes. The standard counterexamples being XOR linked lists, or manual paging with mmap, or manipulating addresses as integers within asm!(), or literally any situation where you can't afford to keep the address as a single value-with-provenance sitting at a known location in program memory until you need it. Strict provenance is sufficient for most use cases, but far from all of them, so there's no viable way to tear the whole concept of exposed addresses out of the language. In any case, removing it would violate basic expectations of stability, given that users have been converting pointers to integers and back since the very beginning of the language. > More pertinently to our discussion, even with PNVI-ae-udi plus a mistake that results in an impossible pointer this is a cause of Undefined Behaviour, which occurs at runtime, it is not a semantic requirement of the language, our Rust program was well formed and correctly translated into machine code if we did this wrong, it's just that it had Undefined Behaviour at runtime as a result of us writing bad unsafe code. My point is that there's no difference in semantics, nor any difference with respect to causality, between an "ill-formed program" that's only ill-formed under certain conditions, and a program with "Undefined Behavior at runtime". The standard ascribes no requirements on the entire execution, start to finish, in either case. But practically, if the implementation doesn't have enough information to distinguish a valid execution from an invalid execution until a certain point (i.e., runtime-dependent UB or ill-formedness), then it must behave properly right up until that point, by the laws of causality. Still, I agree that just calling requirement violations UB would be far less confusing.
- tialaramex 3y ago
  > The standard counterexamples being XOR linked lists, or manual paging with mmap, or manipulating addresses as integers within asm!(), or literally any situation where you can't afford to keep the address as a single value-with-provenance sitting at a known location in program memory until you need it. Well there's a crucial distinction in play here. The XOR linked lists, and some related tricks can be done with address exposure, we expose the pointer and get the integer address, then later when we reconstruct that integer we're allowed to turn it back into a pointer. Rust of course has (as part of the same experiment) APIs for that, you're just paying in terms of worse performance and no tooling (the tooling is disabled if you want these APIs). But the other cases are just voodoo magic, we don't have a model to explain why they should work, which also makes it very hard to, for example, debug them if they don't. They're platform specific. As with the inline assembler, Rust takes no responsibility for whether you can write a correct program in these circumstances, good luck. I don't agree that there isn't a practical difference between IFNDR and UB, I see attempts to confuse these as part of a desire to pretend that C++ isn't markedly worse at correctness than competitors, without the hard work to actually stop it from being markedly worse.

gpderetta 3y ago

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.

LegionMammal978 3y ago

> And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on always telling the compiler what's going on, and as a reward we get both more assurance of correctness because the tools work (Miri for example) and better performance. The experiment is about whether most Rust software can live with this restriction ("Strict Provenance") and the answer IMNSHO is clearly yes. The standard counterexamples being XOR linked lists, or manual paging with mmap, or manipulating addresses as integers within asm!(), or literally any situation where you can't afford to keep the address as a single value-with-provenance sitting at a known location in program memory until you need it. Strict provenance is sufficient for most use cases, but far from all of them, so there's no viable way to tear the whole concept of exposed addresses out of the language. In any case, removing it would violate basic expectations of stability, given that users have been converting pointers to integers and back since the very beginning of the language. > More pertinently to our discussion, even with PNVI-ae-udi plus a mistake that results in an impossible pointer this is a cause of Undefined Behaviour, which occurs at runtime, it is not a semantic requirement of the language, our Rust program was well formed and correctly translated into machine code if we did this wrong, it's just that it had Undefined Behaviour at runtime as a result of us writing bad unsafe code. My point is that there's no difference in semantics, nor any difference with respect to causality, between an "ill-formed program" that's only ill-formed under certain conditions, and a program with "Undefined Behavior at runtime". The standard ascribes no requirements on the entire execution, start to finish, in either case. But practically, if the implementation doesn't have enough information to distinguish a valid execution from an invalid execution until a certain point (i.e., runtime-dependent UB or ill-formedness), then it must behave properly right up until that point, by the laws of causality. Still, I agree that just calling requirement violations UB would be far less confusing.

tialaramex 3y ago
> The standard counterexamples being XOR linked lists, or manual paging with mmap, or manipulating addresses as integers within asm!(), or literally any situation where you can't afford to keep the address as a single value-with-provenance sitting at a known location in program memory until you need it. Well there's a crucial distinction in play here. The XOR linked lists, and some related tricks can be done with address exposure, we expose the pointer and get the integer address, then later when we reconstruct that integer we're allowed to turn it back into a pointer. Rust of course has (as part of the same experiment) APIs for that, you're just paying in terms of worse performance and no tooling (the tooling is disabled if you want these APIs). But the other cases are just voodoo magic, we don't have a model to explain why they should work, which also makes it very hard to, for example, debug them if they don't. They're platform specific. As with the inline assembler, Rust takes no responsibility for whether you can write a correct program in these circumstances, good luck. I don't agree that there isn't a practical difference between IFNDR and UB, I see attempts to confuse these as part of a desire to pretend that C++ isn't markedly worse at correctness than competitors, without the hard work to actually stop it from being markedly worse.