3 ms·

You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. Embedded code in Rust almost always avoids 1, 2, 3, and 4. Arc is

by lambda 9y ago

You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. Embedded code in Rust almost always avoids 1, 2, 3, and 4. Arc is used for freeing dynamically allocated memory when all references, including across threads, are dropped, but if you're running without dynamic memory allocation, you don't need that. Trait objects also require allocation. Embedded targets also generally don't implement stack unwinding, and stack unwinding can be disabled on other targets as well; it's really only most useful in larger applications in which you want some threads to be able to continue running even if another thread panics. Automatic destruction can be fairly easily avoided if you're running without an allocator, as it is mostly used for freeing such allocated memory, as well as a few things like file handles and the like. The things covered in 5 might be harder to avoid, but also more likely to be amenable to being covered by further versions of the RustBelt work. So yes, using a subset of Rust without these features is quite feasible, and often done when working in embedded (aka no_std) code. I don't know SPARK Ada that well, but I believe it has similar constraints of no dynamic allocation. If you can do without dynamic allocation in Rust, many of the problematic features wouldn't be used.

dikaiosune 9y ago
Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
- lambda 9y ago
  Sorry, you are right about that. You can have trait objects without an allocator. I'm not sure how common a pattern that is. Many people like to avoid trait objects and just parameterize the function on a type bounded by the trait in that case. And impl Trait is replacing some of the other cases in which you had to return an allocated trait object. Anyhow, you're right, I was wrong that people couldn't be using trait objects in an embedded context with no allocator, but I also think it's perfectly reasonable to write in a subset of Rust in which you don't use trait objects at all.
  - Argorak 9y ago
    Taking a trait object by reference is a pretty common pattern. Box<Trait> is so pervasive because it's currently the easiest way to get type erasure in return position.
lambda 9y ago
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.

by lambda 9y ago

dikaiosune 9y ago

Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...

lambda 9y ago
Sorry, you are right about that. You can have trait objects without an allocator. I'm not sure how common a pattern that is. Many people like to avoid trait objects and just parameterize the function on a type bounded by the trait in that case. And impl Trait is replacing some of the other cases in which you had to return an allocated trait object. Anyhow, you're right, I was wrong that people couldn't be using trait objects in an embedded context with no allocator, but I also think it's perfectly reasonable to write in a subset of Rust in which you don't use trait objects at all.
- Argorak 9y ago
  Taking a trait object by reference is a pretty common pattern. Box<Trait> is so pervasive because it's currently the easiest way to get type erasure in return position.

lambda 9y ago

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.