I think Idris’s “Elaborator Reflection” and the associated paper Elaborator Reflection: Extending Idris in Idris could be interesting. To make Rust more effective as a host language, you need some way to interact with the type checker I think (but this will expose more of compiler internals of course, which we may not be comfortable with at this stage).
5 Likes