[leafmeal]

As I understand, Lean is a dependently typed programming language. How does it compare to a language like Idris?

How come mathematicians are encoding math in Lean instead of Idris for example?

Someone please correct me, I don't know much about this at all, but I was under the impression that Lean is in a more "imperative" style, while Idris is a functional language. I would have guessed that a functional language would be a better fit for describing math.

[Ericson2314]

I think the "imperative" part is the tactics—metaprogram invocations, the underlying language is still functional.

Idris is geared more towards programming than theorem proving, with the difference basically being that with the latter one cares about more than the types ("I didn't formalize my spec completely") so the specific inhabitant matters. That makes tactics a bit dangerous.

Now there is also a school of thought the finds this reliance on metaprogramming (imperative of other) ugly and a site indication the languages and libraries are not good enough yet. I'm sympathetic, but currently the pro-tactic crowd seems to have the edge.

Lastly, "Lean" is kind of the epitome of "success at all costs" in more ways than tactics: implementation in C++ rather than a nice functional language for dogfooding, willing to sacrifice some intuitionist sacred cows not strictly needed for classical compatibility, etc.

[digama0]

> implementation in C++ rather than a nice functional language for dogfooding

To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure functional) language. The siren song is strong :)

[Ericson2314]

Oh, I did not know that! Will check it out.