Will formal verification ever be possible for systems composed of a bunch of heterogeneous components working together? I'm thinking of a web application, where the software's behavior depends on the interaction of client-side scripts, stylesheets, server-side programs, databases, caching layers, and probably other components, all operating in the request-response cycle that fragments behavior into a bunch of separate runs of the various programs.