Side question: what do you think of Lean? I’m not sure what people who know this stuff think of it. I’ve read comments that say Lean is inferior to OCaml and it simply hyped by celebrity

Yeah a lot of people is shadowing Lean and labeling the success as some sort of marketing success.

I digress from this opinion, mainly because I believe that what truly makes Lean shine is not the language itself but what's around it.

I see Lean as something of a Rust in some aspects. It's a relatively young language, created with a good user experience in mind and a really good environment around it: starting from the VSCode integration, Web support, well written documentation, increasing learning resources and great community. It's just so easy to get started and learn.

At the end there are a lot of other options such as Coq, Isabelle, Agda and others. However, what's around the language is in my opinion more important than specific design decision, and this may be part of the current Lean success.

Interesting perspective. Thanks