> I’d rather have the language …

check out Lean 4 then. Its syntax system is based on Racket but —instead of parens— implements stuff like [JSX syntax](https://github.com/leanprover-community/ProofWidgets4/blob/d...) and a [maze](https://github.com/dwrensha/lean4-maze)