Andrei Alexandrescu:
Why did this redditor say it's a horrific hack? http://www.reddit.com/r/programming/comments/2mqyd3/rust_lifetimes_and_collections/cm6yj7b
For me it's a nice construct, it's something unsafe that the compiler has to "assume" for correct. In a language, unless you want a system like Agda/Coq and you have enough time and brain to write down all proofs, you have limits in what you can express. Sometimes you have to go outside those constraints for various practical reasons, especially in a system language. But I think the unsafety of split_at_mut is all self-contained and you can't go into unsafe territory using it in safe blocks (unlike D things like assumeUnique).
Modern languages are better also because the size of the zone that the compiler can prove as correct is larger. And future languages, with little steps will probably increase such zones, without going to full manual formal proof, that is an excessive burden for most cases for most programmers.
Bye, bearophile
