Ralf Jung has been thinking about semantics of Rust… a lot:

The purpose of MiniRust is to describe the semantics of an interesting fragment of Rust in a way that is both precise and understandable to as many people as possible… Specifically, MiniRust is specified by a reference interpreter that describes the step-by-step process of executing a MiniRust program, including checking at each step whether the program has Undefined Behavior.

Source code here.