> Это не всегда "невозможное". Бывают случаи, когда я могу доказать, что создание
> двух ссылок не нарушит никаких инвариантов, а борроу-чекер не может доказать.
> И это же самый гнусный вариант: если я заткну борроу-чекер unsafe'ом,
> то потом изменения в программе могут привести к тому, что моё
> доказательство станет неверным, и я могу забыть проверить это доказательство. А
> если я буду разруливать по правилам борроу-чекера, то мне придётся переходить
> к динамическим проверкам borrow, что тоже сакс: мало того, что это
> дополнительные тормоза, так ещё и падения программы, происходящие при определённом стечении
> обстоятельств.

Ты конкретного примера пока не привел. Ладно, давай я попробую что-то очевидное.
Для любого положительного целого i, ссылка на диапазон в массиве вида [0..(i/2)] очевидно не будет пересекаться с ссылкой вида [(i/2)..].
Почему бы это не проверять в borrow checker? Ну хотя бы для всех случаев, когда множество из одно range не пересекается с другим?