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.
I'm still not a huge fan of the extra allocation(and chance for cycles) but I stand corrected that it does work, kudos.
It seems like if you have no references in your closure you should be able to pass them around as a value-type(with generics, of course). From what I can tell without that there's a whole range of FP patterns that just aren't representable in Rust because of it.
