Connect to real programming language

Stream: CSLib

[Guchan Li]

Hello! I see from the roadmap that CSLib is aiming for verification in real-world programs. I am curious about the relationship of CSLib and Aeneas, which already translates Rust into Lean. Can these two project be linked somehow in the future? That would be really meaningful for real-world applications. :exploding_head:

[Bas Spitters]

That's what they suggest in the CSLib paper. I'm also curious how it is meant to connect to std.do, which is used by Hax for Rust verification in Lean