Here’s the Deal
Slant is powered by a community that helps you make informed decisions. Tell us what you’re passionate about to get your personalized feed and help others.
When comparing F* vs LEAN, the Slant community recommends F* for most people. In the question“What are the best dependently typed languages?” F* is ranked 2nd while LEAN is ranked 4th.
Ranked in these QuestionsQuestion Ranking
Common Questions
Pros
No pros yet!
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.
Pro Permissive license
Apache 2.0
Cons
No cons yet!
No cons yet!