Rust
Ссылка
нажмите — покажем
нажмите — покажем
🦀 Кто должен доказывать корректность реализации трейта в Rust: сама реализация или код, который её использует?
Нико Матсакис разобрал этот вопрос на примере циклических зависимостей, когда доказательство может замкнуться само на себя.
Допустим, есть трейт Magic: Copy. Любой тип с Magic обязан реализовывать Copy.
Два подхода:
• Модульный: проверяем обязательства при проверке impl. Поэтому impl Magic for String недопустим: String не реализует Copy.
• Внешний: разрешаем такой impl, но при его использовании требуем отдельно доказать String: Copy. Реализация есть, воспользоваться ей нельзя.
Второй вариант помогал обойти проблему циклических доказательств. Но упирался в unsafe-трейты.
Когда автор пишет unsafe impl, остальной код доверяет его гарантиям. Если реализация ошибочно обещает, что Box<T> может содержать нулевой указатель, ответственность лежит на ней.
Выходит странная модель: гарантии безопасности у impl принимаем, а выполнение требований супертрейтов заставляем перепроверять вызывающий код.
Вывод Нико: реализация должна сама устанавливать выполнение своего контракта. Следующая часть будет о том, как совместить этот подход с циклами.
https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/
#Rust
13 · 1.9K ·