Idly wondering if it'd be possible to extend Rust procedural macros with some sort of interface to the name resolver, typechecker, and const eval. Sort of a principled approach to template metaprogramming...
Conversation
1
9
Yeah this stuff is super cool. Also seen in Lean, Agda, and F* I think? Combining this with multistage programming would be super neat as well – not sure if that has been done yet?
1
“A Metaprogramming Framework for Formal Verification” leanprover.github.io/papers/tactic. might be interesting, which documents Lean's approach as of Lean 3, I think? Agda's reflection docs might also be of interest: agda.readthedocs.io/en/latest/lang
Yes, I think Lean developed a similar framework independently, and Agda adopted Idris' approach. I think Lean 4 adds some Racket style macros, which might make it even more applicable to Rust.
2