I'm a big fan of Rhombus' "macros without parentheses", and would love to implement it for my language. Unfortunately, shrubbery notation is just too damn hard to parse correctly, even with a fair number of simplifications. I would have really appreciated some pointers from the paper and documentation about some high-level strategies. Yes, I could technically just use #lang shrubbery, but I'd like to use it outside of racket too

I wish I could get the QoL improvements of mathlib like `lemma` or `ring` without also having to download and compile a significant subset of all of the mechanized mathematics that exist in the world.

I love that Lean supports Windows so well. I run windows on my personal laptop, and it's great to be able to program without WSL. WSL is good, but nowhere near as smooth as native. I compiled a kernel from souce for my WSL to use some additional modules not included with the default WSL kernel, and that has led to WSL shutting down my laptop without warning.