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. These goals are somewhat at odds with each other – the most precise definitions, e.g. carried out in the Coq Proof Assistant, tend to not be very accessible. English language, on the other hand, is not very precise. So my compromise solution is to write down the semantics in a format that is hopefully known to everyone who could be interested: in Rust code. 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.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.