5 ms·
> I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good referen
by pcwalton 5y ago
> I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good reference document.
Zig doesn't have a "rigorous semantic description" that I can find. The reference manual is nowhere close. A "rigorous semantic description" would either be something like that of Java or, ideally, the operational semantics of Standard ML.
I glanced through the "undefined behavior" section in the Zig reference and didn't see use-after-free anywhere. If it's that easy to find missing pieces then it isn't even close to complete. Wait until you start trying to define things like pointer provenance; it's not even clear what semantics LLVM is upholding.
> Having a fancy datalog based borrow checker is cool, but I'd much rather have a formal specifiation of the semantics.
There's a formal specification of the semantics of a subset of Rust via the RustBelt project. These things almost always start with a subset of the language; very few languages have full formal specifications, including type safety proofs and so forth. I should note that I'm not aware of any such work being done for Zig.
> The memory model is not propery defined and only kinda sorta borrowed from C++ as the article mentions.
Where's Zig's memory model? I didn't find it. I did find a GitHub issue [1], which has had far less discussion than that surrounding Rust's memory model.
> I'm sure it would be much easier to add a borrow checker to the well-defined-ness and correctness of Zig, than to make Rust well defined and correct.
No. This is just like the "just add a borrow checker to C++" meme that we used to see until it was shown to be infeasible. The problem is simple: if you can have mutable aliasing today in Zig, which you can, then the ecosystem has surely come to depend on it. So by forbidding mutable aliasing, you will break tons of code. It is not a reasonable subset of code to break; in C++ the set of code you break is "all methods" (because "this" has unrestricted aliasing), and I expect Zig to be no different. The borrow checker is not some magic dust that you sprinkle on a language to make it memory safe; the entire language, including all libraries, must be designed around it. Are you really going to break the doubly linked lists everyone has written?
It is impossible to overstate how much memory safety in Rust is balanced on a delicate precipice; if the language has already fallen off the precipice I'm confident in saying it will never go back. (Well, unless you add a GC, which is what I'd do if I were in charge of Zig. There's nothing wrong with GC; it's the tool people have created for the very purpose of ensuring memory safety with unrestricted aliasing.)
[1]: https://github.com/ziglang/zig/issues/6396 https://github.com/ziglang/zig/issues/6396
- elcritch 5y ago> The problem is simple: if you can have mutable aliasing today in Zig, which you can, then the ecosystem has surely come to depend on it. ... The borrow checker is not some magic dust that you sprinkle on a language to make it memory safe; the entire language must be designed around it. That's a good description of the issue. It's a bit frustrating to see this notion that Zig is "safe" or comparable to Rust in regards to memory safety at all. I don't prefer to use Rust as it's verbose, but at least I realize that if you don't do the lifetime analysis dance in the language you essentially need a GC to manage memory.
- pcwalton 5y ago> I don't prefer to use Rust as it's verbose, but at least I realize that if you don't do the lifetime analysis dance in the language you essentially need a GC to manage memory. Yep. And that's totally valid! I like using GC'd languages; garbage collectors are some of the most successful systems ever developed in computer science.
- elcritch 5y agoIt's true, GC's can often even outperform manual memory management or Rust's lifetime analysis. Having a GC doesn't necessarily prevent a language from being a good system language either. I'm using Nim with its ARC garbage collector on embedded devices and it's been fantastic.
- rocqua 5y agoARC garbage collectors can suffer from reference cycles right? Is that something this Nim configuration suffers from? If so, is it something you noticed in practice?
- elcritch 5y agoYes, it can. In practice most data seems non-cyclic, and Nim has an 'acyclic' annotation to support it. However as Rust has shown, creating non-cyclic async is really hard, and Nim isn't an exception. That means async requires you run ARC with a cycle collector (ORC), and it works on embedded with tweaks. Overall the non-locking ARC + move semantics runs really fast even on MCUs so it's worth avoiding cyclic strctures.