3 ms·
the assumption with Rust is that memory safety (or, generally, resource provenance) is something that needs to exist in the type system. Zig is still young, so
by throwawaymaths 4y ago
the assumption with Rust is that memory safety (or, generally, resource provenance) is something that needs to exist in the type system. Zig is still young, so i would say it's not 100% certain that this shouldn't exist, for example, in a separate step, for example using static analysis.
Rust is already bumping into important cases where the typesystem is incapable of resolving things that "you might want its typesystem to track", and support for these would require breaking all of rust.
Before you say, "static analysis is impossible" -- that's very likely generically true for C (something like Sel4 is in C but gives even stronger guarantees than rust, but IIRC it analyzes machine code). It might not necessarily be. In extremis you could in principle attach a separate file that provides rust function headers for every single function in zig, and checks resource lifetimes inside of each function. So it is not theoretically impossible, just a question of whether or not it's ergonomic and easily accessible.
- monocasa 4y agoFWIW sel4 could have verified the C, they simply decided to verify the machine code so that they didn't have to trust that the compiler correctly complex the verified software. The issue with more broad formal method use is that it's quite a bit of work. The code to be verified has to be designed on the onset for verification, which limits design choices in interesting ways, and even then the verification code far outweighs the code being verified, at about 25:1.
- throwawaymaths 4y agoThank you for the clarification!
- estebank 4y ago> Rust is already bumping into important cases where the typesystem is incapable of resolving things that "you might want its typesystem to track", and support for these would require breaking all of rust. I would be interested in hearing what it is you had in mind. Are you referring to the discussions around capabilities?
- throwawaymaths 4y agoYes, for example. Another dramatic one is the whole parametrized keywords thing, though I guess it doesn't quite "break all of rust".