Итак, в городе появилась новая горячая точка под названием Rust. Давно смотрел и наконец решил посмотреть повнимательнее.
Почитал документы, есть вопросы. Где все документы по теории проверки заимствований?
Все утверждают, что это LTL, но нутром кажется, что фактическая реализация очень далека от линейной или битемпоральной логики. Также есть интригующая инициатива RustBelt (https://plv.mpi-sws.org/rustbelt/), в которой говорится не менее
К сожалению, ни одно из заявлений о безопасности Rust не было официально расследовано, и совсем не ясно, верны ли они.
И есть Wadler et al, но опять же, никаких признаков того, что он имеет что-то общее с реальной проверкой заимствования. Даже статья Microsoft «уникальность, неизменность и безопасный параллелизм» выглядит ближе к Вадлеру, чем к Rust.
Не то чтобы я против ненадежных систем типов… например. TypeScript ненадежен с самого начала; но, по крайней мере, у него есть семантика времени выполнения ES5, а у Rust нет даже этого. Наоборот, у нас есть заявления о надежности, которые основаны на… что за хрень?
Кто-нибудь знает больше?
