> 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 ar

> 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