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.
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.
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.
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.
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.