Rust integration

Stream: general

[Joseph O]

I remember I watched a video a while back of a podcast interview with @Leonardo de Moura ., and they asked him about rust integration, and he answered something along the lines of its planned. I don't remember when this video was posted, but is rust integration still on the roadmap?

[Leonardo de Moura]

Yes, we are still interested, but this only going to happen in the distant future. We have a bunch of higher priority things to work on :(
It would be great if someone volunteers to work on that.

[Henrik Böving]

How would something like Rust integration look like? As in FFI to Rust? similar to stuff like pyo3 or cxx or something different?

[Henrik Böving]

@Leonardo de Moura

[Leonardo de Moura]

How would something like Rust integration look like? As in FFI to Rust?

Yes, the first thing we wanted was a nice FFI to Rust. Right now we have to write wrappers in C.
@Joe Hendrix investigated this issue a bit and may be able to give a better answer.
Then, it would be awesome to have nice support for projects that use both languages. Joe looked into adding support for Lean in the Rust build system.
After we have all that, it would be really amazing if we had support for reasoning about Rust code in Lean.

[Sebastian Ullrich]

My idea was to do FFI on the Rust type system level, which I don't think has been done before. This is only really possible because reference counting allows us to check that Rust affine types are indeed used affinely in Lean (or rather, whenever they cross the FFI boundary), even if we would exchange Rust's compile time guarantees about affine use with runtime panics.

[Sebastian Ullrich]

Though I heard @Marc Huisinga might be interested in improving Lean on that front independently of Rust FFI :)

[Floris van Doorn]

Was this the interview?
https://www.youtube.com/watch?v=XlTiaDqmIsM
Building Better Systems Podcast
Episode # 14: Leo de Moura – Combining the Worlds of Automated & Interactive Theorem Proving in Lean

[Henrik Böving]

We'll I'd love to work on such stuff but you already lost me at affine types so that's a no no for me :P

[Joseph O]

Floris van Doorn said:

Was this the interview?
https://www.youtube.com/watch?v=XlTiaDqmIsM
Building Better Systems Podcast
Episode # 14: Leo de Moura – Combining the Worlds of Automated & Interactive Theorem Proving in Lean

Yeah that was it

[Matthew Ballard]

I would love to help on this but I would need to carried around like a sack of potatoes for a week or two.