Comment by pverheggen
6 hours ago
I have zero experience with formal verification, just speculating here - but could it be because of the network effects?
More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?
Absolutely that's the reason. But the point is the big communities (I'm thinking https://leanprover-community.github.io/ , Kevin Buzzard and all the stuff he's got going at imperial college in the uk etc, the analogous efforts around roq, agda etc which I'm not as familiar with) have made their respective choices and are just getting on with formalising maths. Then there is a vocal minority who want to sit on the sidelines and say they want all these people to use something different from what they have already decided to use. Seems weird.[1]
But yeah it is definitely easier if you just need to formalise the piece you are working on and not invent the whole universe just to bake an apple pie.
[1] And I know it's exactly the same as the people on here and other forums who say other people should down tools on project X and rewrite it in go/rust/zig/whatever. I find that weird also. Like if you want to rewrite a thing in a different language go do that by all means. But saying someone else who develops something in their own time should instead develop a different thing or use a different language is just weird.
I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.