jschwe
commented
10 months ago Please note that I'm not a Maintainer, but realistically speaking I think you would have to do this on a fork. cbindgen currently is only passively maintained by one maintainer with a very limited review bandwidth. On the flipside, there is not too much activity in the repository, so it shouldn't be too much effort keeping your fork up to date.
I'm interested in interop for the lean theorem prover. Rust would be a great candidate for that since lean's memory model is not extremely far from rust's with borrowing, no gc, etc.
Having access to rust libraries would enrich the lean eco system quite a lot and make it a lot easier to use outside of pure theorem proving.
From a quick glance at the code it looks like you already have 3 language backends; C, C++ and CPython.
Would you be potentially willing to accept upstreaming a lean backend, or would I have to work entirely on a fork because you have absolutely no interest.