It may be theoretically possible, but is it ergonomic and useful? Do you use Lean for your programs?

I used Lean for AoC last time and it’s really good.

use https://rocq-prover.org/ for that purpose

Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example.

IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.