Ok, but it looks more like a chicken-and-egg problem. Think about this :
Let's say i create a java/scala/whatever web framework that is even just "30% formally proved" (i know that's pretty vague, but bear with me) : don't you think it would be such a competitive advantage in the corporate world, that it would instantly be a commercial hit ?
Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.
1. This is one of those things where you want it to be all-or-nothing. "30% formally proved" is completely useless; it just means that the inevitable bug or security hole is in the other 70%.
2. You're limited to writing constructs that can be formally verified. (My understanding is that this means that it's a bit more difficult than "let's formally verify Ruby and then run all the Ruby programs on our verified Ruby"; some programs will need to be rewritten and others will simply not be verifiable.)
3. We still have to solve the politics problems that already are pervasive in some of these environments (e.g. people who intentionally leave easy bugs in their code and then fix them later so that they look like they made more changes as measured by a KLOC count).
I want to qualify your (1) a bit—there's actually enormous value in "partially proved" systems in a sense. At the very least, that 30% is something you won't have to think about every again so long as the spec it's met works for what you need.
But what I really wanted to talk about is the exciting stuff going on in languages like Idris where programming is paramount and proving is just there for support. In a situation like this, your goal is less to arrive at 100% formally proven systems, but instead steal 90% of the power of a proof assistant to build more maintainable, powerful code. In this case, you're quite likely to only prove 30% of your code, the skeleton perhaps, and leave the rest. The result is often however that when you do this, the remaining 70% of the code is so restricted by your design that there are only a handful of ways to continue and they're likely all the right behavior.
A great example of this is Ur/Web which uses just a little bit of dependent typing to ensure that the names in your forms, domain, and databases all match up. It means you design your entire system around those names (your domain) and prove it to be formally consistent. Then the remaining design space is tiny and it's easy to write a good program.
... Or even to augment that skeleton with a security policy and have static flow control analysis "for free".
(That said, Ur/Web is a prototype system with minimal documentation, so I won't recommend it as an actual "system of the future"... just a glimpse.)
Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.