[userbinator]

and for a lot of programmers math seems to be an unapproachable alien language

is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program

I think the main problem is that it's too formal. Turning something that is really about simple logical deduction into thick abstract maths is sure to dissuade the majority of the people who might find it useful. The elitist gatekeeping attitude that cryptographers tend to have doesn't help either.

[mecsred]

A problem here is that it's not a simple logical deduction being converted to "thick abstract math". The math is the proof. A formal proof is necessary to verify the deduction.