[esafak]

Is this useful for specifying programs too or only theorems?

[zeckalpha]

Curry-Howard correspondence.

[esafak]

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

[siknad]

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.

[tsterin]

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

[nymalt]

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