Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.

What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.

[1] https://fstar-lang.org/

[2] https://fstarlang.github.io/lowstar/html/Introduction.html