Yes I was surprised how capable Lean 4 is for general programming.

I know, I have written about Idris before, but I have not used it for a while.

Glean is getting a lot of buzz, it is on my to do list. :D