Математически доказанная безопасность Rust — это как?

Question

[Имя Фамилия]

Здравствуйте.

Недавно увидел сентенцию, мол, "безопасность Rust имеет математическое обоснование". Кто-нибудь может подсказать, о чем идет речь?

Comments

[sim3x]

Линк?
Почему вопрос не задан автору фразы?

[Имя Фамилия]

sim3x, где-то на хабре, ссылку потерял. А вопрос не задал потому, что на хабре у меня read-only аккаунт.

[Moskus]

Tommy Gain, личные сообщения, тем не менее, вы там посылать можете.

[Имя Фамилия]

Moskus,

где-то на хабре, ссылку потерял

Да, я бы мог отправить личное сообщение.

[crazyh]

Надо полагать, кто-то решил поумничать и придумал такую формулировку для обозначения того, как работает система владения и подсчет заимствований: по сути, при успешном компилировании выполняется уравнение `количество_заимствований - количество_возвратов_заимствований = 0`. =)

Answer 1

[Tyranron]

Процитирую humbug из комментов к недавней статье:

Конкретно в https://people.mpi-sws.org/~dreyer/papers/rustbelt... формально доказывается, что система типов Раста, владение, заимствование и прочее — корректны. Доказывается, что программа безопасна, если написана на безопасном подмножестве Раст. Доказывается, что программа безопасна, если в ней есть вкрапления unsafe, в которых программист не допустил ошибки, UB.

Кроме того, проект RustBelt на текущем этапе занимается формальной верификацией библиотеки std, но полная проверка требует времени. Поэтому библиотеку проверяют по кускам. Да, были найдены и исправлены 2 ошибки в unsafe коде (что показывает, что ребята делом занимались), тем не менее все эти thread, mutex, Arc/Rc формально безопасны.

Собственно, сами математические доказательства смотрите в научных публикациях:
RustBelt: Securing the Foundations of the Rust Pro...
KRust: A Formal Executable Semantics of Rust
K-Rust: An Executable Formal Semantics for Rust

Сайт проекта RustBelt: plv.mpi-sws.org/rustbelt

Answer 2

[Yo JLa]

Рабочая группа есть, когда будут результаты? Наверное не быстро..
https://github.com/rust-lang-nursery/wg-verification

Цели и задачи группы перечислены
https://rust-lang-nursery.github.io/wg-verification/