Нужно понимать, что в статье, которую ты читал, авторы Cedar сознательно выбрали стратегию «двух дорожек» (две кодовых базы: модель на Lean и производственный код на Rust) и стыковали их не формальным доказательством эквивалентности, а дифференциальным тестированием. То есть они в Lean создали формальную модель (и доказательства её свойств), а потом в Rust написали «боевую» реализацию и проверили, что на миллионах случайных тестов оба варианта ведут себя одинаково. В результате они получили практически надёжную гарантию того, что продакшн-код совпадает с моделью, но не «математически железобетонное» доказательство эквивалентности.
Почему именно дифференциальное тестирование, а не формальное доказательство?
Сложность Rust. Язык Rust (особенно с учётом системы владения, жизненных времён и т. д.) довольно нетривиален для формальных доказательств. Вообще существуют научные проекты, которые пытаются формализовать Rust вплоть до машинной модели (например, RustBelt в Coq), но пока нет «из коробки» готовой инфраструктуры, чтобы автоматически связать Lean-модель и реальный Rust-код и формально подтвердить, что они совпадают.
Практические ограничения. Даже при наличии формализации Rust можно столкнуться с тем, что часть кода в Cedar «слишком большая» и включает сторонние библиотеки, системные вызовы, unsafe и т.д. Формальное доказательство всех таких участков потребует огромной работы и зачастую выхода за рамки Lean (или Coq). Дифференциальное тестирование проще масштабировать на весь код.
Быстрота итераций. Подход, описанный авторами, удобен для быстрого обновления. Когда дорабатывают модель или Rust-реализацию, они заново прогоняют тесты (их миллионы) и быстро смотрят, нет ли несовпадений. Если бы у них была цепочка формальных доказательств «Lean→генерация→Rust», это бы тоже пришлось сопровождать и поддерживать, что может оказаться тяжелее, чем переписать кусок кода и прогнать тесты.
Таким образом, даже несмотря на то, что Lean даёт формальное доказательство корректности модели, сами авторы Cedar не пошли по пути полного формального доказательства для Rust-кода. Они использовали Lean-модель скорее как «идеальную спецификацию», а Rust — как высокопроизводительную реализацию, а связь проверили дифференциальным тестированием.
Могли бы мы формально доказать соответствие кода на Rust и модели на Lean?
Теоретически — да, но это потребует:
Формализовать подмножество Rust (и его семантику) внутри Lean (или, как минимум, в каком-то инструменте, который можно связать с Lean). То есть нужно иметь детальное описание того, как именно интерпретировать конкретную программу на Rust (с учётом всех языковых особенностей).
Выполнять либо ручной рефакторинг, либо автоматическую генерацию Rust-кода из Lean. Если бы мы генерировали Rust из Lean по «доверенному» транслятору (который сам формально доказан), то итоговый Rust-код автоматически совпадал бы с моделью. Но на сегодня в Lean нет «из коробки» генерации в Rust (есть подобная генерация в Coq, Isabelle, F*, но даже там Rust-путь пока экспериментальный и неполный).
Либо же доказывать уже на уровне Rust (то есть брать существующий Rust-код и формально показывать, что он эквивалентен Lean-модели). Такая «трансляция» требует формального определения: «Если программа P на Rust скомпилирована в машинные инструкции, то при каждом входе x поведение программы совпадает с поведением Lean-модели M(x)». Плюс нужно доверять компилятору rustc, что он не внесёт ошибок. Иными словами, это уже очень тяжёлый проект по полноформатной верификации компилятора и кода.
В академических кругах ведутся исследования, как подмножества Rust можно доказывать тем же Coq (RustBelt и др.), или как писать «проверяемый Rust» (проект Verus, Kani и т.д.), но пока нет готовой цепочки «Lean→Rust с доказанной эквивалентностью». Так что Cedar-подход — это практическое компромиссное решение: просто проверять равенство результатов на огромном наборе тестов.
