The post is kind of funny to be honest. It’s a lot of contorting to say they just want to use something which they feel is newer and more hype.

I think this quote encompasses the whole thing:

> Admittedly the abstractions in the above code probably make it a bit slower than the comparable OCaml one, but the nice thing about Lean's metaprogramming support is that in theory, we could incrementally introduce our own optimisations into the pipeline

Yes, the OP dislikes Ocaml because the compiler is conservative so you can reason about run time performance so you might want to rewrite in a less pretty but more efficient style. Lean is better because while the performance is worse all the time they _in theory_ maybe could be better using meta programming.

Not that I have anything against Lean, it’s a very cool proof assistant with a bright future. I’m not sure I would put forward what the author puts forward to sell it though.

AI generated proofs in Lean are a sight to behold and probably reason enough to get interested.

oh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs.

Things like:

- bindings to godot (https://github.com/kiranandcode/lean4-godot)

- advent of code (https://github.com/kiranandcode/lean-aoc)

- ffi bindings to constraint solvers (https://github.com/kiranandcode/cleango/)

Obviously a slightly biased selection here, but the key point is to clarify that it's more than feasible to use it for real programs that do all sorts of non-mathy stuff.