9 ms·

Zig's approach is really nice here, but it's also a notably easier problem to solve than rust has, since it's not trying to solve for parallel/concurrent safety

by skohan 5y ago

Zig's approach is really nice here, but it's also a notably easier problem to solve than rust has, since it's not trying to solve for parallel/concurrent safety. Do you think Zig's approach would be feasible in Rust? I guess maybe you could do it, but the sync version would have to have the stricter constraints of the async version.

dnautics 5y ago
I'm holding out for formal-methods based static analysis on lifetimes in zig.
- pcwalton 5y ago
  Not possible for the same reasons why just adding a borrow checker to C++ isn't possible. Mostly this comes down to incompatibility with existing code. Zig is just not memory safe, and the only solution would be to add a GC.
  - surajrmal 5y ago
    If you don't consider Swift style Automatic Reference Counting a GC, then there is another option.
    - pcwalton 5y ago
      That's a form of garbage collection. :)
    - skohan 5y ago
      The problem with ARC in swift is that it’s always atomic. This is fast enough on ARM, but on x86 it’s really slow
  - dnautics 5y ago
    This is a very bad take. By your argument there's no reason why sel3 should exist, which is written in C and safer than rust.
    - pcwalton 5y ago
      Assuming you mean seL4, that was formally verified by taking a manual specification of the L4 kernel and laboriously proving that the C code implements that specification. That is not at all what the compiler's lifetime/borrow check subsystems do for Rust. They know nothing about what the program is supposed to do; they only check that some relatively-simple rules are followed. That's why Rust requires so much less effort on the part of the programmer than formalisms that aim to prove programs correct.
      - dnautics 5y ago
        Nobody is arguing anything on the level of doing a full on Sel4 -- but Sel4 does have generalized no memory leak, no uaf guarantees as a subset of all specification proofs, so my point "memory safely is possible to bolt onto even C" is still valid.
    - kobebrookskC3 5y ago
      feel free to keep writing c, as long as you prove all your code memory safe. i'm gonna take a stab and say writing rust is easier.

by skohan 5y ago

dnautics 5y ago

I'm holding out for formal-methods based static analysis on lifetimes in zig.

pcwalton 5y ago
Not possible for the same reasons why just adding a borrow checker to C++ isn't possible. Mostly this comes down to incompatibility with existing code. Zig is just not memory safe, and the only solution would be to add a GC.
- surajrmal 5y ago
  If you don't consider Swift style Automatic Reference Counting a GC, then there is another option.
  - pcwalton 5y ago
    That's a form of garbage collection. :)
  - skohan 5y ago
    The problem with ARC in swift is that it’s always atomic. This is fast enough on ARM, but on x86 it’s really slow
- dnautics 5y ago
  This is a very bad take. By your argument there's no reason why sel3 should exist, which is written in C and safer than rust.
  - pcwalton 5y ago
    Assuming you mean seL4, that was formally verified by taking a manual specification of the L4 kernel and laboriously proving that the C code implements that specification. That is not at all what the compiler's lifetime/borrow check subsystems do for Rust. They know nothing about what the program is supposed to do; they only check that some relatively-simple rules are followed. That's why Rust requires so much less effort on the part of the programmer than formalisms that aim to prove programs correct.
    - dnautics 5y ago
      Nobody is arguing anything on the level of doing a full on Sel4 -- but Sel4 does have generalized no memory leak, no uaf guarantees as a subset of all specification proofs, so my point "memory safely is possible to bolt onto even C" is still valid.
  - kobebrookskC3 5y ago
    feel free to keep writing c, as long as you prove all your code memory safe. i'm gonna take a stab and say writing rust is easier.