如何手工给出形式化证明？是否有一种语言规范，像形式逻辑一样形式化，我们可以在此基础上建立我们的证明？
例如，如何知道this modulepanic是否为s？

mod my_mod {
    use std::marker::PhantomData;
    
    #[derive(Clone, Copy)]
    pub struct A<'id> {
        p: PhantomData<*mut &'id u8>,
        data: u32,
    }
    
    pub fn scoped<T>(data: u32, f: impl for<'id> FnOnce(A<'id>) -> T) -> T {
        f(A {p: PhantomData::default(), data})
    }
    
    impl<'id> PartialEq for A<'id> {
        fn eq(&self, other: &Self) -> bool {
            // Can we prove that this assertion will never failed whatever code is using this mod?
            assert_eq!(self.data, other.data);
            // some UB stuff if the assertion failed here
            true
        }
    }
}

Rust playground
这个非常具体的例子背后的直觉是在变量上给出类型级别标记（作为一个生存期泛型），这样我们就可以保证两个A<'id>总是从同一个源复制。