My practitioner view of program analysis

The gap between formal and informal has been pointed out as an Achilles' heel of formal methods from the dawn of the field, so critique is not particularly new. The standard reference is Social processes and proofs of theorems and programs (1979), which is worth reading.

the author seems unaware of the SAT/SMT solver/analysis ecosystem