[abstractcontrol]

Having been inspired by that video by Kevin Buzzard and finally finding something that would be worth formalizing, I am trying out Lean at the moment. I have about 2-3 months of Coq experience, so I can say that even without the quotient type, Lean is much better designed than Coq. I can't vouch for how it will do at scale since I've only started it out, but from what I can see, Lean fixes all the pain points that I had with Coq while going through Software Foundations.

It has things like structural recursion (similar to Agda), dependent pattern matching (the biggest benefit of which would be proper variable naming), unicode, `calc` blocks, good IDE experience (it actually has autocomplete) with VS Code (I prefer it over Emacs and the inbuilt CoqIDE is broken on Windows), mutually recursive definitions and types, and various other things that are not at the top of my head.

If I were to sum it up, the biggest issue with Coq is that it does not allow you to structure your code properly. This is kind of a big thing for me as a programmer.