О формальном доказательстве безопасной работы с памятью на основе «владения и заимствования»

info@vsetut.pro

Стать автором

Вернуться

07.03.2025 14:55:34 | Хабр

Хабы: C++, Rust, Алгоритмы, Математика, Программирование

Некоторое время назад я попробовал найти формальное доказательство безопасной работы с памятью, которое реализовано в Rust, но так и не смог его найти. После чего у меня сложилось впечатление, что доказательство в формальном виде и вовсе отсутствует, а вся концепция безопасного управления памятью на основе "владения и заимствования" формально не доказана и держится только на честном слове.

Я не являюсь специалистом по Rust, но после просьбы помочь разобраться этим вопросом, был переадресован искать эту очевидную информацию самостоятельно, так как "джентльменам верят на слово". Тогда как косвенным подтверждением моего предположения об отсутствии формального доказательства в общем виде, является тот факт, что отсутствует и полный список разрешающих и/или запрещающих проверок, которые реализованы в самом компиляторе языка.

Я хочу рассказать про изыскания о формальном доказательстве безопасной работы с памятью на основе владения и заимствования (не зависимо от языка программирования или реализации компилятора), которое основано на собственных данных и рассуждениях.

Читать дальше →

Подробнее