8 ms·

Curry-Howard correspondence.

• esafak 3mo ago
  It may be theoretically possible, but is it ergonomic and useful? Do you use Lean for your programs?
  • tsterin 3mo ago
    use https://rocq-prover.org/ https://rocq-prover.org/ for that purpose
  • nymalt 3mo ago
    I used Lean for AoC last time and it’s really good.
  • siknad 3mo ago
    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.