I'd implore anyone interested in metaprogramming to look at Lean4
It gets overshadowed by the theorem proving but it's unsurpassed in metaprogramming, to my knowledge it can do anything Lisp Racket and Rhombus can and much more
I was curious about the meta programming in Lean4 so I poked around a bit. [1] It’s hard to judge a complex system from a quick glance.
I don’t know about power, but the syntax was noisy. (It’s hard to judge how important that is.)
Can anyone comment more? Does the meta-programming stuff get exactly the same checks as regular programming? What kind of error messages do you get from parse failures when your metaprogramming code is being used?
I don't think this is true. Lean has hygienic macros, but doesn't appear to have local macros like Racket does; the thing called "local macro" restricts a macro's use to a certain region, but the macro definition can't capture local variables from outside of it.
Related. Others?
Rhombus Language 1.0 - https://news.ycombinator.com/item?id=48633473 - June 2026 (113 comments)
Summer Rhombus picture competition 2026 - https://news.ycombinator.com/item?id=48546270 - June 2026 (3 comments)
Rhombus Language - https://news.ycombinator.com/item?id=43394881 - March 2025 (158 comments)
Rhombus: A New Spin on Macros (2023) - https://news.ycombinator.com/item?id=42041070 - Nov 2024 (1 comment)
Rhombus: Macro-extensible language with conventional syntax built on Racket - https://news.ycombinator.com/item?id=41151439 - Aug 2024 (97 comments)
State of Rhombus (programming language) - https://news.ycombinator.com/item?id=30314109 - Feb 2022 (17 comments)
I'd implore anyone interested in metaprogramming to look at Lean4
It gets overshadowed by the theorem proving but it's unsurpassed in metaprogramming, to my knowledge it can do anything Lisp Racket and Rhombus can and much more
I was curious about the meta programming in Lean4 so I poked around a bit. [1] It’s hard to judge a complex system from a quick glance.
I don’t know about power, but the syntax was noisy. (It’s hard to judge how important that is.)
Can anyone comment more? Does the meta-programming stuff get exactly the same checks as regular programming? What kind of error messages do you get from parse failures when your metaprogramming code is being used?
[1]: https://leanprover-community.github.io/lean4-metaprogramming...
I don't think this is true. Lean has hygienic macros, but doesn't appear to have local macros like Racket does; the thing called "local macro" restricts a macro's use to a certain region, but the macro definition can't capture local variables from outside of it.