Open Kernel Labs clamed to produce the world first 100% verified "bug free" software. Some ~8,000 lines of code were subjected to scrutiny of "over 10,000 intermediate theorems in over 200,000 lines of formal proof" to make sure that the software is "functionally correct".
By functional correctness they mean that "the implementation always strictly follows a high-level abstract specification of kernel behavior."
As saying goes, the chain is as strong as its weakest link... Applied to software world one could be tempted to paraphrase: a software stack is as robust as its weakest component. But software system is more than sum of its components. By virtue of interdependence, a software-intensive system includes everything - from server to network to software to user... And all of these parts change - not only by themselves but also in response to the changes occurred in other parts. Say a faulty memory chip will lead to application's working memory set corruption which introduces instability into the system... What good would be a perfectly correct code if it cannot execute? What if the "high-level abstract specification of kernel behavior" was flawed to begin with?
This brings me to the same dilemma I've been pondering in my cozy data world: it IS possible to have perfectly correct data yielding absolutely incorrect information... I sense that Gödel's Incompleteness Theorem is lurking here somewhere…
The product releases should be in meaningful increments, each release potentially becoming the last in line. This gives the customer (even if the customer is you) a sense of control, and produces a relatively self-contained system at each release...And a possibility to call it quits at any release time.
Branching, in my opinion, is not for release but rather for investigating alternatives; they will either be merged back into trunk, or abandoned. The last thing you need is multiple versions of the product floating around...Every release should be tagged, and - if there were changes to the environment -wrap up the envirionment (VM), and store it alongside with the product.