>The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.

I think most problems that one would encounter professionally would be difficult to formally specify. Also, how do you formally specify a GUI?

>The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.

I think we have to ask what exactly are we trying to formally verify. There are many kinds of errors that can be caught by a formal verification system (including some that are in the formal spec only, which have no impact on the results). It may actually be a benefit to have proofs separate from code, if they can be reconciled mechanically and definitively. Then you have essentially two specs, and can cross-reference them until you get them both to agree.