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).
=> More informations about this toot | View the thread | More toots from gigapixel@mathstodon.xyz
=> View math tag | View tla_plus tag | View coq tag | View rocq tag | View stream tag | View Lean4 tag | View rust tag This content has been proxied by September (3851b).Proxy Information
text/gemini