There's an inside baseball discussion happening here with the larger Rust community that I think, maybe, you're missing. You are absolutely correct in saying that Go, Python et al offer memory safety in a way that low-level languages do not. These languages use techniques that incure some kind of runtime penalty. Erlang, for instance, copies memory like it's going out of style. Now, with Rust you get a similar kind of memory safety but, somewhat uniquely, without the same category of runtime penalty. There's still some, sometimes, and that's where the community discussion around 'unsafe' happens in Rust.
So, you're writing in Rust and you'd like to write code which has the absolute most aggressive performance possible. In Rust parlance this _maybe_ means you need to do unsafe things: turn off bounds checks, fiddle with the raw memory of a structure, allow multiple threads to access the same memory without synchronization, interact with mutable globals and so on. That's great, but, you've potentially opened up your program to crashes or security issues. If you're a solo author that's a trade-off you can make based on your needs. Here's the rub: if you use similar techniques in a crate -- a shared library for all to use -- then you've opted everyone using your crate into the same trade-off, one which they might not have otherwise chosen for themselves. What the Toshi project is saying here is that it's design preference is to avoid opting into this trade-off, preserving all the guarantees that Rust can provide at _possibly_ the expense of absolute performance.
There's a safety-focused subset of the Rust community that takes the presence of an 'unsafe' in a body of Rust code very seriously and this project is participating in that conversation.
This is very well stated. I would clarify one thing in particular. I think, hard to speak for everyone, most people have settled on the idea that high-level libraries should avoid unsafe (like this one) and rely on libraries that need to work around safety restrictions.
This allows the “unsafe” libraries to have fewer lines of code and more isolated testing, with greater coverage.
You can also, if they're written in C, verify the absence of everything you'd worry about using the automated and lightweight tooling available for C. Then, fuzz it to be sure. Then, port it back to equivalent rust maybe with C2Rust. Then, equivalence testing to make sure the two have same output. That's my current recommendation for medium-assurance apps in Rust that have to use unsafe code. Oh yeah, gotta turn overflow checks on in the safe Rust for best effect but might have performance hit.
I'm still thinking about the rest of concurrency problems and side channels that Rust's type system doesn't cover. Trying to find out what's as easy as above. For concurrency, I'm eyeballing Eiffel's SCOOP, DTHREADS, and eventually will study whatever Pony is doing.
> You can also, if they're written in C, verify the absence of everything you'd worry about using the automated and lightweight tooling available for C. Then, fuzz it to be sure. Then, port it back to equivalent rust maybe with C2Rust.
Not sure I totally understand (or if I do, totally agree). For all FFI in Rust, we have to drop down to unsafe interfaces. I like the model that's generally happening in this area where there is an auto-generated sys crate (with bindgen), then an FFI crate that does all the Rust <-> C interop. This tends to work pretty well.
A lot of C/C++ (native library) validation tools just work with Rust artifacts, so I don't personally see a lot of value for writing in C as well as Rust, unless we're talking about a rewrite from C to Rust.
> still thinking about the rest of concurrency problems and side channels that Rust's type system doesn't cover.
What things are you thinking about beyond the Send/Sync traits? I've found those to be very expressive, and appropriately restrictive.
"A lot of C/C++ (native library) validation tools just work with Rust artifacts,"
Tools like RV-Match and Astree Analyzer can prove absence of entire classes of errors using static analysis. Frama-C and SPARK Ada can do that with annotations with high amount of proof automated. There's optional, runtime checks for stuff not proven if you don't want to or can't do it by hand. C also has lots of open-source tools for static/dynamic analysis, test generation in many forms, and so on. In my Brute-Force Assurance concept, you convert a program into C and/or Java to throw all the automated tooling you can at them, fixing whatever real issues are found. Then, the last benefit is C has a formally-verified compiler should someone want to eliminate compilers as an error source. Rust-to-C is still valuable for all these reasons.
So, is the Rust tooling at the level that you can do all that without converting it to C?
"What things are you thinking about beyond the Send/Sync traits? I've found those to be very expressive, and appropriately restrictive. "
I don't use Rust yet. I just know what I learn from folks like you who do. When I studied it, the docs said their type system blocked some but not all concurrency problems. I don't know where it's at currently on various types of races, deadlocks, and livelocks. Those are the main problems improved models or analyzers should try to solve.
But comparing Rust to C is difficult. On the one hand they compile down to the same thing, on the other when not using unsafe, the type system itself allows you to express strong proofs, especially with state machines.
I don’t generally need to make use of these tools, I would point you to the ring project, where they are very interested in formal proofs: https://github.com/briansmith/ring they might have some interesting options and a few of the people over there are very capable in answering these questions.
> I don't know where it's at currently on various types of races, deadlocks, and livelocks.
For dataraces, there is a very strong story. In terms of deadlocks, I’m not aware of anything here. For livelocks, I think it’s generally possible define the state of a system such that you can make sure you aren’t in conflict with other threads, so better, but not fundamentally different than other threaded languages. In other words, if you define cross thread state in an appropriate way, you can prove that you can’t get into a livelock situation.
I was in that comment section bringing up RV-Match. The difference is that RV-Match is a bunch of static-analysis functionality built on a comprehensive semantics for C. KRust is a tiny subset of Rust with RV-Match-style analysis. I did bookmark it in case it could be useful for someone trying to build that.
"where they are very interested in formal proofs"
The only thing I mentioned that would be doing a formal proof was the lightweight stuff like Frama-C and SPARK Ada that don't require proof so much as annotation (eg like borrow checker) that run through automated provers. The rest was all push-button or no-proof-needed tools that say something has no errors, specific errors, or a mix of them and false positives. RV-Match and Astree Analyzer will straight-up tell you that specific errors don't exist with low, false positives. The test generators that work on structure of your code get deep into lots of errors from different combinations of inputs and control flow. None of these require proof. People building these usually test them on FOSS projects, sometimes the same ones, often finding new errors in them.
"In terms of deadlocks, I’m not aware of anything here. "
Good to know. That be the focus area for now since you said livelocks are a good situation. I'll still keep an eye on the side for anything checking that.
"they might have some interesting options and a few of the people over there are very capable in answering these questions."
So, you're writing in Rust and you'd like to write code which has the absolute most aggressive performance possible. In Rust parlance this _maybe_ means you need to do unsafe things: turn off bounds checks, fiddle with the raw memory of a structure, allow multiple threads to access the same memory without synchronization, interact with mutable globals and so on. That's great, but, you've potentially opened up your program to crashes or security issues. If you're a solo author that's a trade-off you can make based on your needs. Here's the rub: if you use similar techniques in a crate -- a shared library for all to use -- then you've opted everyone using your crate into the same trade-off, one which they might not have otherwise chosen for themselves. What the Toshi project is saying here is that it's design preference is to avoid opting into this trade-off, preserving all the guarantees that Rust can provide at _possibly_ the expense of absolute performance.
There's a safety-focused subset of the Rust community that takes the presence of an 'unsafe' in a body of Rust code very seriously and this project is participating in that conversation.