I disagree with you whemently.
Two or three, or seven, computers do not help if there is a SW bug. And don't give me "separate teams making different SW" bullshit, it has been proven that they all make the same mistakes.
Formal proving? It is neither necessary and the assumptions the proof takes are usually far too lenient.
The web browser, while complex, should not be designed so that every line of code is potential security breach - so big a hole that just looking at a textual input will give attacker whole access to your computer. Are you really claiming that using proper runtimes (managed, "jail", unprivileged, ...), proper compartment (only minor amount of code can have security effect, ect.) a safe browser cannot be done relatively easily? It might require twice the effort to write, but then it would require half the effort to keep up.
You will never secure a computer as long as you use C/C++ - that I agree.
What they did wrong with Java, I don't know, have not been following. It must have been huge architectural and desing and programming culture flaw.