I should also add that while you can do a lot of this subsetting, I wouldn't be surprised if some of these issues were already covered by the time the rest of R

I should also add that while you can do a lot of this subsetting, I wouldn't be surprised if some of these issues were already covered by the time the rest of Rust has been formally modelled and verified enough to be a competitor to Spark. That is, what RustBelt analyzes right now is a language which has an analogue to Rust's borrow checker, but is much much simpler overall; and they ported Rust's implementation of several types of shared mutable or owned references over to this language to verify them. There is a lot of Rust outside of these few caveats that hasn't been covered; these are just the things which could be in scope of the RustBelt work that haven't been covered by it. Here are a few things that there's ongoing work on that you would want to finish before saying you were confident in a using a formally verified language: 1. The memory model. This gives a formal definition of what kinds of aliasing assumptions the compiler is able to make about raw pointers in `unsafe` code. This is being worked on here: https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model 2. The borrow checker. While the RustBelt work shows that a much simpler borrow checker can be sound, Rust's borrow checker has to deal with a much more complicated language, and there are few known soundness bugs in it (discussed elswhere in this thread). You'd want that to be formally modeled and verified. 3. The type system. Rust has a fairly full featured type system, so you want to ensure that's sound 4. The compiler itself. Even once you have sound code in a sound language, you need to make sure that the compiler follows the rules and compiles it correctly. 5. Any libraries or code that you are using which might be using `unsafe`. The RustBelt work so far has done so for a few core primitives, as well as a couple of third-party libraries, but of course you'd want to re-do this work against the full language (or a real-world subset, not LambdaRust that this paper used) and include any other libraries that you might need to use. So, I'd say that there's a good chance that the RustBelt work could be extended to include one or more of these listed features before all of the rest of the above has been done. It will be a while before you could have a usable, verified subset of Rust, but once you do I think it could be a good alternative to something like SPARK, or development in C following extremely stringent rules and compiling with CompCert.