Theory and practice of proof carrying code in Rust