We currently describe Rust's memory model via axioms. We might want to instead create a Lean object which represents the Rust memory model and implicitly inject this as a conjecture in all of our proofs instead of literally introducing it as an axiom.
We currently describe Rust's memory model via
axioms. We might want to instead create a Lean object which represents the Rust memory model and implicitly inject this as a conjecture in all of our proofs instead of literally introducing it as anaxiom.