I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.
Lean is also a lot faster.
Lean is also a lot faster.
What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?
Because from what I understand Rocq too has Gallina or something right?
I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.
What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.