What do the Rust people think of that idea? And how hard would you guess an AutoCorres-style tool be for it vs C in event we wanted HOL parts?
For C, you just need to come up with a restricted semantics for a subset of C (e.g. you can pick a particular evaluation order, assuming your implementation also respects it). Rust is a much more complex language, with no formal semantics forthcoming, and you would need to verify the semantic properties supposedly enforced by the type system, as well as their interaction with unsafe code. All of this would require new deep research, whereas the equivalent for C-like languages is well-trodden ground by now.
Actually, €5MM grant has been given to some academics to produce a formal model of Rust over the next few years. So we'll see... A big part of it is also formalizing what unsafe means, which is the hard part.
That's what my Googling showed me. Good call. SPARK, C subsets, and embedded Java still winning in this area.
Don't get me wrong, great language but I'm a but dubious of the 1:1 porting story here.
Stuff like this is one of the trade-offs in Rust: control over exactly how closures behave (if allocations are necessary, if virtual calls are necessary when calling it) is balanced with/detracts from how much typing one needs to do to get them to work.
