Imperative programming, and aliasing in particular, represents a major
obstacle in formally reasoning about everyday code. By utilizing restrictions
the imperative programming language Rust imposes on mutable aliasing, we
present a scheme for shallowly embedding a substantial part of the Rust language into the
purely functional language of the Lean theorem prover. We use this scheme to
verify the correctness of real-world examples of Rust code without the need
for special semantics or logics. We furthermore
show the extensibility of our transformation by incorporating an analysis of
asymptotic runtimes.
Publications
Advisors
Students
