Hacker News new | ask | show | jobs
by pron 1600 days ago
> Rust treats correctness as paramount, not just memory safety... Zig doesn't.

I strongly disagree.

> but the language doesn't make any efforts to make it easier than any others.

Of course it does. Correctness is Zig's greatest emphasis, and so the language includes several important correctness features: explicitness (e.g. no overloads, no implicit calls), fast partial compilation, easy testing. Neither Rust nor Javascript have these important correctness features (Comparing Zig's explicit simplicity to JS is just as wrong as comparing its soundness to C. Zig is much sounder than C and much more explicit than JS. Zig is so revolutionary and different from everything else that we have little if anything to compare it to).

It's just that Zig's approach to correctness is different from Rust's. It relies less on soundness and more on simplicity. As someone who's been involved with formal methods for some years, I can tell you that even in that community, there are these two approaches, those who prefer soundness, and those who prefer ease, as two valid approaches to correctness. The soundness camp wants to eliminate certain bugs; the ease camp wants to find as many bugs as possible per unit of effort. I think all agree we need some combination of the two, but where the best sweetspot(s?) is (are?) is an open problem. We do know that there is a tradeoff between the two. To increase ease you must either remove soundness or offer soundness to eliminate a more restricted set of bugs. For example, sound static analysis covers fewer issues than full-blown "deep" sound proofs or model checking in exchange for greater ease, and concolic testing might uncover deep logic bugs, but at the expense of soundness.

> all Zig is 100% unsafe by default

That's incorrect.

> And unless Zig adopts a borrow checker or find an equivalent alternative...

You are defining the notion of correctness to coincide with what Rust does (i.e. sound memory safety). As Zig's correctness is handled completely differently (broad strokes: find less memory safety bugs, find more others), this makes your point tautological.

Both Rust and Zig have the same emphasis on correctness and the same dedication to features that support it — some help soundness, others ease — but their balance between the two, how they try to achieve correctness and by catching which bugs is different. We don't yet know which, if any, of these languages offer a better path to correctness. And if our assumption is that more soundness always equals more correctness, then neither of these languages are in the right direction, as both intentionally sacrifice a great deal of soundness — almost all of it, really — in the name of ease.