2 ms·

If the halting problem were decidable, we wouldn't need to rewrite the world in Rust; we could write a checker for C that would anticipate all memory safety vio

If the halting problem were decidable, we wouldn't need to rewrite the world in Rust; we could write a checker for C that would anticipate all memory safety violations of an arbitrary C program at compile time.

musicale 2y ago
> we could write a checker for C that would anticipate all memory safety violations of an arbitrary C program at compile time. I think that's called a "memory safe compiler". There have been multiple examples (SoftBoundCETS[1], Safe-C, Fail-Safe C, etc.) as well as partial/incremental solutions (-fbounds-safety, CheckedC, etc.) An irritating problem with C is that it is underspecified, so many "working" C programs rely on unsafe operations that would be flagged as errors by a memory safe compiler. [1] "Full Spatial and Temporal Memory Safety for C", https://people.cs.rutgers.edu/~sn349/papers/safety-sp-2024.pdf https://people.cs.rutgers.edu/~sn349/papers/safety-sp-2024.p...
- musicale 2y ago
  Following up I note that you said "at compile time". Usually C programs have data-dependent behavior, which necessitates runtime checks (but generating those checks is an example of "anticipating memory safety violations.") Symbolic execution can potentially identify possible data-dependent memory safety violations, and it has been used in compilers and code checkers, but it can also become intractable (algorithm may be decidable, but the compute and memory requirements may be too high.)
anyfoo 2y ago
The problem is with defining what a “memory safety violation” is. By the time you’ve annotated all the code with the information necessary to tell what you find undesirable up to rust’s capacity (e.g. overstepping buffers, violations of move semantics…), say through a type system that allows you to express these requirements, and have spent the time to change the parts of the program that did not fit with your new more restrictive types… … well congratulations, you’ve just written your program in a language that effectively is rust.

musicale 2y ago

> we could write a checker for C that would anticipate all memory safety violations of an arbitrary C program at compile time. I think that's called a "memory safe compiler". There have been multiple examples (SoftBoundCETS[1], Safe-C, Fail-Safe C, etc.) as well as partial/incremental solutions (-fbounds-safety, CheckedC, etc.) An irritating problem with C is that it is underspecified, so many "working" C programs rely on unsafe operations that would be flagged as errors by a memory safe compiler. [1] "Full Spatial and Temporal Memory Safety for C", https://people.cs.rutgers.edu/~sn349/papers/safety-sp-2024.pdf https://people.cs.rutgers.edu/~sn349/papers/safety-sp-2024.p...

musicale 2y ago
Following up I note that you said "at compile time". Usually C programs have data-dependent behavior, which necessitates runtime checks (but generating those checks is an example of "anticipating memory safety violations.") Symbolic execution can potentially identify possible data-dependent memory safety violations, and it has been used in compilers and code checkers, but it can also become intractable (algorithm may be decidable, but the compute and memory requirements may be too high.)

anyfoo 2y ago

The problem is with defining what a “memory safety violation” is. By the time you’ve annotated all the code with the information necessary to tell what you find undesirable up to rust’s capacity (e.g. overstepping buffers, violations of move semantics…), say through a type system that allows you to express these requirements, and have spent the time to change the parts of the program that did not fit with your new more restrictive types… … well congratulations, you’ve just written your program in a language that effectively is rust.