3 ms·
By proving that memory references don't live longer than the allocated memory. The use of dynamic allocation must be carefully restricted and programmer may ne
by Nokinside 9y ago
By proving that memory references don't live longer than the allocated memory.
The use of dynamic allocation must be carefully restricted and programmer may need to provide provide assertions or modify the code to pass verification.
There is two ways tho think static verification:
1. Language level verification. All valid programs are verified to be correct in respect of safety guarantees the language gives.
2. Verification of safety features that can't be proved in general. In most cases it's possible to write program in a way that it can be verified to be correct, but finding a way to write provably correct program may need some work.
- pjmlp 9y agoNow try to use that in the presence of commercial libraries.
- jhasse 9y agoTry to use Rust in the presence of commercial libraries.
- pjmlp 9y agoEasy just like any compiler for a memory safe language. There might exist logical bugs, but the language semantics allow for a higher thrust of code quality, assuming the binaries haven't been tampered with. Every line of C code is unsafe, specially if the binary was compiled with -O3. Regarding Rust, the only issue is lack of support for binary libraries in Cargo, one needs to call rustc directly.
- Rusky 9y agoLinux doesn't do any of this, and doing so is tantamount to running a borrow checker on the code, which requires more information than is present in vanilla C.
- pcwalton 9y agoAt that point you will have basically reinvented Rust. The resulting language will be so incompatible as to essentially be a new language.