Hacker News new | ask | show | jobs
by vicpara 1242 days ago
Why on earth they had to invent a new language with another crazy syntax that reinvents everything? With such an incredible team at MSR that did everything from new languages and compilers, couldn't they have know better?
2 comments

Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html) and explain to me how that "reinvents everything".

There are several new and non-trivial things going on in this language! Look at the papers about hygienic macros, or functional-but-in-place, or any of the others.

What specifically is crazy about Lean's syntax?