![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Значит, есть такой новомодный язык Rust. смотрел я на него, смотрел, и решил наконец подчитать.
Подчитал, возникли, эммм, вопросы. Где какие-то пейперы по теории, лежащей под borrow checking'ом?
Все декларируют что это, вроде как, LTL, но по ощущениям фактическая реализация не укладывается ни в linear logic, ни в bitemporal logic.
Есть еще такая шикарная инициатива RustBelt ( http://plv.mpi-sws.org/rustbelt/ ), в которой написано, ни много ни мало, что
> Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold.
Есть wadler et al, но нету вообще никаких ссылок на то, что оно с фактическим растом имеет хоть что-то общего. Даже майкрософтовский пейпер "uniqueness, immutability and safe parallelism" кажется ближе к вадлеру, чем раст.
При этом не то чтобы я имел что-то против unsound type systems... тот же тайпскрипт unsound от слова "совсем"; но под тайпскриптом хотя бы рантайм семантика ES5 есть, а тут нету. Напротив, есть soundness claims, но wtf, на чем они основаны?
Кто что знает еще?
Подчитал, возникли, эммм, вопросы. Где какие-то пейперы по теории, лежащей под borrow checking'ом?
Все декларируют что это, вроде как, LTL, но по ощущениям фактическая реализация не укладывается ни в linear logic, ни в bitemporal logic.
Есть еще такая шикарная инициатива RustBelt ( http://plv.mpi-sws.org/rustbelt/ ), в которой написано, ни много ни мало, что
> Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold.
Есть wadler et al, но нету вообще никаких ссылок на то, что оно с фактическим растом имеет хоть что-то общего. Даже майкрософтовский пейпер "uniqueness, immutability and safe parallelism" кажется ближе к вадлеру, чем раст.
При этом не то чтобы я имел что-то против unsound type systems... тот же тайпскрипт unsound от слова "совсем"; но под тайпскриптом хотя бы рантайм семантика ES5 есть, а тут нету. Напротив, есть soundness claims, но wtf, на чем они основаны?
Кто что знает еще?
