Comment by kleiba2

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean.

Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.