> TL;DR: Yes! But Zig is a Stand-in for simpler languages, and while in its infancy, I can foresee it to be "done" and "fit into my head". I don't understand h

> TL;DR: Yes! But Zig is a Stand-in for simpler languages, and while in its infancy, I can foresee it to be "done" and "fit into my head". I don't understand how something that isn't type-safe (memory safety is a subset of type safety) can be more "correct" than a language that is type-safe. It is certainly hard to prove Rust type-safe. But that's infinitely easier than proving something type-safe that trivially isn't type-safe! > way to much fondness of abstractions and their removal by compiler magic Heavy reliance on abstractions is what makes lifetimes and the borrow check practical. For example, Arc, Mutex, Cell, and RefCell are all abstractions that serve as library-defined extensions of the core lifetime rules and are generally optimized away by the compiler. I'm extremely skeptical that lifetimes/borrow checking can be made usable without this sort of thing. If a goal of Zig is to minimize abstractions, then that's yet another reason why adding a borrow check to it after the fact will not work. When Zig is "done", it will have to either (a) become memory safe by addition of Rust's lifetimes/borrow check (which is probably impossible, but if it were done it would bring about a lot of the things you say you don't like about Rust); (b) become memory safe by addition of a GC (which is the best option, but I doubt it will do so); (c) not be memory safe (which is probably what will happen). There is no free lunch. And then, assuming it chooses option (c), you run into this problem: Try as hard as you want, you will never be able to prove a language type-safe that isn't type-safe, no matter how simple that language is.