I thought that after three decades of programming for a living I would eventually stop writing buggy code. Well, yes and no. I made a lot fewer, but there were still a few embarrassments.
Then my good friend and colleague, Dr. Allan Stavely of the Computer Science Department here at New Mexico Tech, got an NSF grant to study a new methodology called Cleanroom Software Development. Since this intensive class, he has twice taught a 3-hour course in the methodology, and I got to take it in the spring of 1994.
At this writing (in the fall of 2002), I have embraced this style in all my coding projects, large and small. Almost all this coding has used Python, with some Icon, a little emacs Lisp, and even some XSLT.
My strong feeling is that this is the way to go, and I will never go back to my older, sloppier, bug-prone ways of developing code.
The best source for practicing the method is to read Dr. Stavely's book:
Stavely, Allan M. Toward Zero-Defect Programming. Addison Wesley, 1999, ISBN 0-201-38595-3.
My employer, New Mexico Tech, also offers a three-credit, 400-level Computer Science course in the method. This course is great for learning to apply the principles to practical problems.
The name comes from analogy with the cleanrooms of wafer fabrication plants. Rather than trying to clean the crud off wafers after they are made, the object is to prevent the dirt from getting into the fab environment in the first place. Similarly, with the Cleanroom method, the aim is to write the code correctly the first time, rather than trying to find the bugs once they are there.
This method steers a nicely balanced course between the extremes of correctness proofs and no methodology at all. The originators (principally the late Harlan Mills) claim that the method produces highly robust code without taking any longer than the traditional software lifecycle. Proportionally, much more of the time is spent in design.
Here is an extremely sketchy outline of the methodology:
This is a stepwise refinement method, so we start by describing the intended function for the system as a whole, and refine until all the primes are verified, all the way down to the terminal modules.