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-mathem

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/ https://fstar-lang.org/ [2] https://fstarlang.github.io/lowstar/html/Introduction.html https://fstarlang.github.io/lowstar/html/Introduction.html