The formal verification subject is tricky. For a lot of software (especially in the web startup world) it is often not possible to hire someone trained in formal methods to perform extensive checks/proofs on software which undergoes rapid change as the company pivots every couple of months.

Functional programming alone doesn't give you any guarantees about safer or more correct software than any object oriented language unless you ruthlessly exploit its type-system. Even if you do, the specs have to exist upfront and they have to be correct and stable. One can make the case that isolating side effects and capsuling them in a controlled structure is "the right thing" to do, but that alone does not give you any formal verification of your program.

From personal experience I can only say that whenever I brought up formal verification because of security/correctness concerns, I was immediately shut down by business, because it's simply too expensive for software that doesn't control life-critical systems.

I think with security (and esp. privacy), the problem is more coming up with the specs in the first place. If you can do that in a reliable way, designing appropriate static analyses is probably doable.

What I see is Ada picking up steam after being people getting fed up with C like exploits every day.

http://www.his-2014.co.uk/programme.html

Or C being so limited, that it just looks like Ada with C syntax.

http://www.misra-c.com/Activities/MISRAC/tabid/160/Default.a...