Service orchestration. Instead of thinking of a Web page that displays search results, we can think of two features: A Web service that performs a search and a bit of code that formats search results in HTML and displays them to a browser. Breaking the coupling of the work and testing components individually greatly reduces the complexity of each piece. In essence, two divided by two becomes less than one.
Yes, service orchestration might fail when the service is down because, say, a SysAdmin accidentally changes a firewall or router rule--but formal proofs don't offer a solution there, either. There is a chance, though, that the problem could be caught in a collaborative environment. These techniques support each other.
What's Next? Better Frameworks, More Collaboration
In his keynote address at the 2009 Google Test Automation Conference, Wirth said industry advances in proofs have been disappointing and the problem of testing is likely to be with us forever. Over the past decade, these problems have become more complex, as desktop software for one product line or operating system has given way to a half-dozen Web-browsers and dozens of mobile device manufacturers with hundreds of model numbers.
Testing problems are likely to be with us for years to come. Nicollete's suggestions of more powerful frameworks, more collaborative environments and the separation of work into services that can be tested independently may at least create an environment where code demonstrates that it can work under precise conditions.
While provably correct code may be a Pied Piper not worth following, today, organizations can make strides to radically improve software quality before it gets to exploratory testing. That is something to celebrate--and to keep moving forward.