4 ms·
> The checker needs a few simple theorems, such as "valid_array(A,0,n) and valid_element(A[n+1)) implies valid_array(A,0,n+1)" to check this. This is basically
by Manishearth 10y ago
> The checker needs a few simple theorems, such as "valid_array(A,0,n) and valid_element(A[n+1)) implies valid_array(A,0,n+1)" to check this.
This is basically dependent types. Rust doesn't really want to go that far from a language level.
> Handling these two classes of unsafe code takes care of a sizable fraction of the unsafe code really needed in Rust.
Not really. All the other datastructures in the stdlib would still need unsafe. Not really a good metric.
The Rustbelt project at MIP-SWS is doing formal verification of Rust including unsafe code, and that approach will be far better IMO. It won't let you eliminate unsafe from your code, but might make it easier to prove that your unsafe code is performing safe operations.
- dbaupp 10y ago> FWIW you can use Weak for this. There's a performance cost though. The sentence before your quote mentions ref-counting. This is referring to Weak.
- Manishearth 10y agoSomehow missed that, thanks.
- deleted 10y ago[deleted]
- Animats 10y agoAll the other datastructures in the stdlib would still need unsafe. Why?
- Manishearth 10y agoHow would you implement the robin hood Hash{Set,Map} with this? Or BTreeMap? Maybe I misunderstood your proposal, at first it seemed like dependent types (which makes vectors awesome but really doesn't address other things), but your Pascal thing makes it sound more like complete formal verification, which is what Rustbelt is doing. I don't expect that to become part of the language (maybe? would be cool), but it would help reason about unsafe code.
- comex 10y agoYou can implement a hash map safely on top of an array; indeed you could do it with `Box<[T]>` today. You would just miss the optimization where missing buckets can be represented by zero in the "hash value" field rather than an explicit Option.
- Animats 10y agoDoesn't Option() on a Rust pointer optimize down to a zero pointer value anyway? Much of the unsafe Rust code I come across looks like either premature optimization or trying to write C in Rust.
- Manishearth 10y ago> Doesn't Option() on a Rust pointer optimize down to a zero pointer value anyway? There aren't pointers here though. But yes, you could use NonZero<T> to mark the hash value as never-zero so that the option gets optimized. You'd still need unsafe code to construct the nonzero, but that's okay. At least for the Hashmap I don't think the code is premature optimization; it seems to be pretty "idiomatic" unsafe Rust, with unsafe used exactly where needed. I haven't really looked at the btreemap in a while.
- Animats 10y agot seems to be pretty "idiomatic" unsafe Rust, with unsafe used exactly where needed. I haven't really looked at the btreemap in a while. The number of excuses associated with unsafe code in Rust is excessive.
- Manishearth 10y agoIt's not an excuse, I just don't think that your statement that the hashmap code uses unsafe superfluously is correct.
- 10y ago