Rust is a general-purpose, memory-safe programming language with the aim of providing guaranteed safety regarding manipulating, reading and storing data. Currently, there is no formal specification for the Rust compiler. Without the behaviour of Rust defined, how do we know that our code has sound behaviour? This project takes a small step towards a formal treatment of the Rust compiler by formalising a fragment of the intermediate language MIR, and hand-proving the correctness of a simple optimisation.

MIR (Middle Intermediate Representation) is the language of the Rust compiler’s frontend, post-type checking and prior to translation to LLVM IR. Several MIR-to-MIR optimisations take place in the complier. One such optimisation, ‘simplify branches’, eliminates dead branches in conditionals with constant value conditions. We provide a grammar for a fragment of MIR sufficient to express a set of programs that the optimisation targets. We provide a formal semantics for this MIR fragment, a formal definition of simplify branches, and hand-prove the soundness of simplify branches. This exploratory work makes a first step toward verification of the frontend to the Rust compiler.