ghost code

А вот вам вкусного из реддитов.

Новое понятие "ghost code". Это код, который добавляется в программу каким-либо препроцессором/аугментатором/доказателем/ассистентом, который гарантировано уничтожается при компиляции, но который может добавлять утверждений для компилятора для валидации. Грубо говоря, способность компилятора выкидывать мёртвый код используется для того, чтобы записать набор желаемых свойств для объектов, которые заставляют компилятор больше работать и больше проверять.

Источник: https://www.reddit.com/r/rust/comments/1ainrpg/i_wrote_my_masters_thesis_about_rust_verification/