4 ms·
From the perspective of this software engineer, Lean seems mostly superior to the other proof assistant languages. You can develop in a regular text editor, the
by lacker 6y ago
From the perspective of this software engineer, Lean seems mostly superior to the other proof assistant languages. You can develop in a regular text editor, the source code is open, you don’t have any hacky “some expressions are a sublanguage in string constants” stuff, and most importantly the community is extremely responsive. Speed is the biggest problem; Lean 3 still has a very slow interpreter and it makes some things (in particular communicating out to an external specialized solver like the “hammer” tactics) too slow to be practical. If Lean 4 manages to improve speed as much as promised, and the 3 -> 4 migration actually happens, I think it will become the all-around superior choice.
- mcguire 6y agoFrom the perspective of this software engineer, "the 3 -> 4 migration actually happens" was the part of the article that was most disappointing.
- lakecresva 6y agoThe Lean developers put out a paper about v4's reference counting last year which shows that in basic benchmarks, Lean 4 is in the same ballpark as Haskell, Swift, and ML. https://arxiv.org/abs/1908.05647 https://arxiv.org/abs/1908.05647