LEAN Review

3 0

Review of LEAN powered by the Slant community.

Ranked in these QuestionsQuestion Ranking

What are the best dependently typed languages?

Pros

Pro
Interactive tutorial runs in the browser

Lean has a JavaScript version you can try online. (And a faster C++ version you can download.)

Pro
Visual Studio Code support

Lean is a Microsoft Research project, so they have their own IDE support.

Pro
Emacs support

Pro
Metaprogramming occurs in the same language as the theorem proving.

Because the metaprogramming occurs in the same level as the programming, you are able to write automated tactics that depend on mathematical objects you have already defined, and use those tactics to define more objects. It is a very powerful leap forward in automated and interactive theorem proving.