Correctness by Construction (CbyC)

I read "Correctness by Construction: A Manifesto for High-Integrity Software" at first with excitment on what they did right (seeing the chart with low error rate per line of code). However after I read the formal methods stuff I started to check out. This is only meaningful if the end product is well known and clear specificiation is possible. It is only good for new projects as well, since taking and changing existing code (which is where most of the money is spent in the industry) requires different approach.

I'm looking for ways to allow big picture ideas to be sketched out and then step wise refined while keeping the original ideas easy to maintain and update. Requirements change over time and tools/language/process have to deal with the ever changing world.

[Funny how "Free Agent Nation" points out that only school systems/buildings have kept the same look and feel of 30 years ago unlike businesses and even govmnt offices.]