Rust is a systems programming language with mutable and shared borrows, which are restricted notions of references giving respectively a read & write and a read-only access to their underlying value. Rust type system ensures that values can be either mutated or aliased through borrows, but not both at the same time. This eliminates a large class of errors and allows to reason more easily of the behavior of such programs.

Aeneas is a framework exploiting those guarantees to give Rust programs a high-level semantic, by translating it to a pure functional program. We build upon results from Aeneas to explain and extend this translation, while preserving the linearity present in Rust programs.