Picked up from Slashdot, an article at IEEE about a British software house delivering code with less than one error per ten thousand SLOCs, albeit at a premium of up to 50% higher costs than regular development. Their “secret” is to return to the roots of software engineering by describing the application in terms of a a formal specification language Z (“zed”) based on set theory and predicate logic before subjecting it to mathematical analysis to identify ambiguities and inconsistencies, and only then converting it to code (which itself becomes a relatively trivial task). Incidentally, they code in Spark, a descendant of Ada, and if you follow that link to the Wikipedia article you’ll see an example of some excellent commenting techniques under “Annotation Examples”.
Accurate and complete requirements gathering is emphasised, as is prototyping as a means of requirements feedback to the customer. In an example development described in the article the developed software showed just four faults in the first year of operation out of 100,000 SLOC.
I found the IEEE article rather inspiring, although at the end the comments on the willingness of programmers to use formal methods and logic are depressingly familiar.
There are more details in a presentation by Praxis here.