> This isn't in any way related to the claim that I qualified as “very strong”: you said “But my point was that that reasoning isn't additive”, which is a very strong claim and likely to be false.

You've misunderstood. I am not trying to make a claim about how reasoning works, but to give possible explanations for why assumptions that more soundness is always better often turn out wrong, i.e. how it could work. The question of why it is that we get such "surprising" outcomes in software correctness is interesting, but we until we get an answer to it, we just know that we get surprising answers.

> I'm just arguing that at this point your reasoning of saying “we don't know which is better” is as fact-based

This doesn't make sense at all. Not knowing is the default. Until there's conclusive evidence, the fact is that we don't know.

> Too bad, I won't have a single example of how Rust incurs a cost in correctness

I don't know that it does. I gave you several examples of how it might: reading it is hard as it has implicitness and compiling it takes long making testing more burdensome. Maybe there are other reasons, maybe there are none.

Now, this is handwaving, but it's more than we need. It's okay to believe that Rust yields more correctness than Zig, the same amount, or less, but until we have empirical findings one way or the other, we don't know, even without any handwaving.

> nor how Zig's design is so brilliant it will make thinking about memory more practical than C and avoid memory management to get in the way of correctness

I explained that, too. Not only does Zig provide sound spatial memory safety -- which neither C nor C++ do -- but it also has precise pointers, i.e. you can soundly track where your pointers are, which is not the case in C/C++, where you can magically create bad pointers from good ones with pointer/array index arithmetic, or magically create pointers from non-pointers with silent casting (like unions). Zig, like Rust and GC languages has precisely tracked pointers. Good pointers can turn bad through user-after-free in Zig, but they can't be "born" bad as in C and C++.

> Where in my comments can you find a single occurrence of this claim?

Not in yours. In pcwalton. You've just tried inverting the rules of science by saying that if you assert something is true and someone else points out that it's an unsubstantiated hypothesis, the burden of proof is on them, thereby making your hypotheses true by default.

Again, I think there can be a wide consensus that both Zig and Rust provide more correctness than C or C++ because they both make stronger sound guarantees and neither is worse at reasoning or testing than C++, but the question of whether any of them is more effective at correctness than the other is unknown, and unknowable until we empirically compare the two. That something is unknown is not a claim that requires proof; until we have proof for something -- we don't know.

Here's what happened with Haskell: Some Haskellers kept insisting that Haskell yields more correctness than some other languages, and that that should be accepted as the null hypothesis until proven otherwise. Then there were a number of empirical tests that believed they'd be able to show it, and they couldn't find any large effect. So even after the empirical examination some Haskellers insisted their hypothesis should be taken as true by default, because the empirical tests weren't good enough. The result is that people who care to claim about correctness get sucked into these beliefs and not even empirical findings (or lack thereof) can shake them. That's not how we move correctness forward. Of course, Rust is not quite in the same position as Haskell because it hasn't been around the long, but it's important not to get too attached to religious beliefs that "this is the only way." Findings in software correctness frequently surprise us.