One of the big potential synergies between #rust and #lean4 rely on the rust type system which is sound (https://en.m.wikipedia.org/wiki/Type_safety). I have a long ongoing project proving liveness properties for a collection of parallel and concurrent #stream processing combinators. Rust’s type system should allow guaranteeing liveness for these combinators at compile time. But it is not rich enough to prove liveness in the first place. And that’s one reason I got interested in lean. Other languages crossed my mind like #rocq (formerly #coq) and #tla_plus but lean won out for its rich math library, connections to the #math community, and great tooling (like nvim integration).