> No. The claim "design with tradeoffs X leads to more correct programs than design with tradeoffs Y" is the one that requires evidence. The null hypothesis is that it doesn't.

What's the argument here? Is it OK then to question the existence of the Apollo program because “the yanks never went to the moon” is the null hypothesis?

We've plenty of evidence that Rust offers better guarantees than C (even though with your reasoning there could be a hidden second-order effect that makes Rust actually worse than C, we cannot be sure after all, the Rust compiler is slower than C's… /s).

Now since Zig doesn't address the most prominent source of critical defects in C, the null hypothesis is that it won't be an improvement compared to C. (I actually don't think that hypothesis is true either, C is very dated and there are tons of room for small UX improvements, but getting an improvement as big as what Rust offers is a big step to climb with small improvements).

> As I said, software correctness is my thing. When I saw Zig's brilliant, revolutionary design, I thought

Yet you're like two thousand words in and you've not even begun to hint at what part of Zig designs makes it especially good for correctness compared to C.

> However, anyone who says we already know is not telling the truth, and probably has a shaky understanding of the subject.

Like with climate modeling or immunology, we're far from knowing as much as we'd like, but that doesn't mean we know nothing: for instance we know that 1) distributed systems are practically impossible to get right without tools (and TLA+ is a blessing), and we know that 2) manual memory management isn't tractable by a human without assistance. For these two problems, we have decades of empirical evidence that shows that the human brain just isn't able to do it reliably. We also know that 3) so far sanitizer and other runtime tools haven't been enough to get it right in practice.

Zig basically says that even if 2) is true, 3) will not hold for long because it will have “better tools”® than what exists for C. Hard to tell how far these tools will eventually go, but for the moment it has yet to prove anything on that front.

> You're saying it's not good because it doesn't try to completely eliminate such errors?

Yes I am, because ”eliminating completely* such errors” is the standard for every language designed after 1985 that has reached even limited use. (And we're not talking about some low-level stuff that only C or C++ could do, but about a product that competes with another written mostly in JavaScript).

By letting this kind of errors happen, it's a step back of more than 35 years ! And by “happen” or “completely eliminate” I mean “happen enough that it surfaces significantly to the user” (and resp.), I'm not arguing that it should be proven that it cannot happen (in fact, even Rust does make such a claim),but at least it should be exceptional in practice, not one of your most common issue keyword on github…

If Zig empirically had like 0.1% memory issues, then arguing that improving on any other fronts is more important would be fine (like Go not being memory safe in the presence of data race, we can agree that this isn't a significant factor in software reliability using that language and move on), but it's not what's happening. What happens is that the only commercial use of Zig so far is facing a double-digit amount of memory-related crash reported by its users. We're not talking about CVEs found by an adversary here, just Joe the user who has his software randomly crashing at startup. Correctness you said?

> Zig's memory safety story is not perfect because the cost of perfection, Zig's philosophy believes, is too high, to the point of working against the goal of correctness.

As a side note, this is a strawman, Rust doesn't aim at ”perfection” either as it's happily relying on unsafe code when needed, and Rust pragmatic solution to improving memory safety in unsafe code was Miri, a runtime sanitizer, not some kind of proof assistant or anything). There's also a runtime check for overflows or out of bounds access, not dependent types to aim at soundness perfection.