3 ms·
> Do you make extensive use of `unsafe` Rust? Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidab
by orlp 5y ago
> Do you make extensive use of `unsafe` Rust?
Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers.
I use no other special (unstable) features, just pointers and ptr::copy(_nonoverlapping).
> If you would ever be interested in a collaboration proving your algorithm correct let me know :)
I might take you up on that, or at least ask you to take a look once I'm done polishing the code.
- xavxav 5y ago> Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers. Ah, that's frustrating, my tool Creusot is meant for the verification of safe code, though I also worked on unsafe code verification as part of the RustHornBelt project (upcoming PLDI paper). I'd still love to chat and see how far we can push verification, you can reach me via email at xldenis @ lri . fr