This is so true, I’ve basically done, the same at work I really like C, I’ve rewritten a firmware at work from C++/python to pure C, and it’s really nice, but the only reason i did that, is because I’m the only developer on that firmware, so C is great because it’s my C (and it’s the secret first step for another rewrite to zig).
But for the backend code which used to be in python, we have chosen Rust (instead of C/C++) because it makes collaboration easier between the people who rarely touch the backend code (me), and those who maintain it.
6 Likes
The borrow checker didn’t invent memory safety. seL4, CompCert and SPARK Ada achieved certified safety without one. They did it by making code so explicit that proofs become practical.
Zig is the first mainstream language built from the ground up with exactly that DNA. We’re not “behind” Rust on safety. We’re on an orthogonal, historically proven path.
The real flex would be a comptime-powered verification subset (think SPARK but powered by Zig’s comptime). There’s even been discussion about it since 2020. Who’s working on that?
10 Likes
That’s still requires demarcation of covariance and contravariance, and lifetimes, correct? Zig is already quite verbose, wouldn’t writing contracts, marking input/output, and with lifetimes turn it into, effectively, Rust? I really wish we could avoid that fate.
I’m reading that SPARK ensures exclusivity via SMT solver that runs before the compilation even starts, how slow is that process? I’m reading they are NP-complete, are there algorithms to reduce it to at least O(N log(N)) w.r.t. the number of tokens being analyzed?
Will it still support doubly linked lists and graphs? Or, those become impossible, like in Rust?
I’d rather settle on run-time memory safety checks (valgrind style), Garbage Collector (unlikely to be supported by Zig directly though), or Nim’s YRC. And I’m quite happy with valgrind overall, and hope that ASAN’s support will improve as Zig 1.0 is shipped.