I believe the hard part of building software to be the specification, design, and testing of this conceptual construct, not the labor of representing it and testing the fidelity of the representation. We still make syntax errors, to be sure; but they are fuzz compared with the conceptual errors in most systems.
Yes!!! Consider the recent Mars Spirit Rover problem... it was an unconsidered scenario, not an ill-specified proof, that disabled the Rover.
We need *simple* tools that stay out of the way for us to have more time to consider problematic scenarios.
And we need better simulation tools and conceptual analysis tools. For example was Spirit's flash file system modeled at any level as a concurrent state machine? What kind of analysis would have caught the missing transition from a failed transmission to expunging the leftover files?
Note that this is also what Longhorn architects should fear the most... the unknown unknowns, as Rumsfeld would put it.