Rudra VS electrolysis

If you’re writing unsafe Rust, you might consider cargo miri and Rudra as additional static analyzers which can find bugs rustc won’t

In my opinion, much of Rust-specific PhD research likely to be publishable and/or high impact either falls into verification (e.g Prusti, Cruesot) or bug-finding (e.g. Rudra, SyRust). Ralf Jung and his collaborators have done exceptional work in the verification space.

Perhaps Rudra as well.

Haven't used it myself, but I remembered a tool called Rudra was recently posted about in the sub

Not sure proves your point, but maybe doesn't disprove your point strongly enough. I am not qualified to argue from experience about how Rust is ideally suited in the ways you think it is not. But from everything I have seen, it can do a whole lot of what C++ is also good at. Rust safety is not all or nothing and a codebase could definitely prioritize ergonomics over correctness.

Two things that I saw in the last couple weeks that might start to sway you.

https://github.com/sslab-gatech/Rudra#readme

GhostCell: Separating Permissions from Data in Rust

How do you represent this?

However, this insight holds for relatively common forms of ownership, and you can see this exploited in electrolysis: https://github.com/Kha/electrolysis

In my opinion the best way of going about it is translating the Rust to Coq that has the same semantics (but different performance) as pioneered in https://github.com/Kha/electrolysis. Unfortunately that project isn't usable today as it requires an ancient version of Rust and Lean.