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.