> 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."
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.