Rust lifetimes and collections [OT]

[bearophile via Digitalmars-d]

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