That's what hooked me on Lean. Lean is a general-purpose software development language, not just a formal verification language. This is powerful.