Formalizing the high-level language would have some difficulties, e.g. the trait system has a lot of ad-hoc complexity, and there are convenience features like automatic destructors that improve programmer productivity but greatly complicate the definition of things like evaluation order (which is currently undefined for Rust). These things make the specification more complex, but they appear to be well within the limits of current programming language technology. For example, the safe subset of Rust could possibly be translated into a relatively standard type system with linear regions, e.g. http://www.cs.cornell.edu/people/fluet/research/substruct-re....
The difficulty comes at the semantic boundary, where the state-of-the-art in modeling the interaction between distinct languages is still far away from the safe / unsafe portions of Rust. This is an interesting research project, and fits in well with a general trend of cross-language interaction that appears in current research on programming language formalization. However, because it requires formalizing something that includes a C-like language, it's hard to imagine it ever being any simpler than formalizing a C-like language. If you're a user of unsafe code and just want to prove that the unsafe code is "memory-safe" (a somewhat nebulous term), then this helps you out. But if you're going to prove that your entire program is correct, why bother with all of the extra complexity?
