The article is not a big deal but the comments were really interesting, especially all the PhD's in Computer Science who said following formal methods would make it all better, plus the usual folks who want regulation and certification and licensing.
All I could think of was "good luck with all that". After 30 years of writing code for a living I feel secure in saying that there is no silver bullet, no magical method or paper guarantee that will make all software perfect and bug free.
In fact it's even difficult to define what a program is, much less describe how you would go about developing perfect programs. Software lives in so many realms, is written in so many environments, languages and businesses, and interacts in multitudinous and often unpredictable ways that there isn't any easy way to even find a formal definition of what comprises software. Try to find common ground between iPhone games, high speed stock trading systems, your toaster and a Mars lander. Try to license programmers in Assembly, C, Java, PHP, Fortran, LISP and Erlang. Now add multiple language web applications and client/server and distributed systems.
That's one mighty bunch of stuff to try to describe formal methods for; just listing all the programming languages is mostly impossible much less explaining how to write perfect code in all of them.
I love when people try to compare programming to something like civil engineering. Building a bridge has not fundamentally changed in two thousand years; you deal with gravity, wind, rain and heat and many basic materials that would be familiar to a Roman engineer. In programming we have to create our own universe for every program, or probably a better description would be we adapt some collection of universe elements that are combined to simultaneously construct a hundred different bridges which all have to work together even though the universe may change unpredictably later.
Even worse is that a bridge may take years of planning and construction time, and then last for a 50 years without alteration. Software evolves constantly, both during development and afterwards. There are around 600,000 bridges in the US, built over two centuries. There are nearly a million iPhone apps all of which were written in the past 5 years. Programs come in all sizes from a few lines of code to tens of millions and touch every single area in modern life.
What makes writing software so hard is that it can be almost anything and anywhere, affect one person or a billion, have to work flawlessly for decades or only once. It's nothing like a bridge or a building. The Mars Lander is millions of lines of C written for exactly one use. High speed stock trading software executes trillions of times one microsecond at a time.
The idea that there exists a set of formal methods that if followed ensures a perfect result for every kind of program is ludicrous. Even if such a perfect miracle were possible the cost would make it impossible to ever use it. Even if you could formally prove a set of source code where would it run? An operating system you don't control? Calling web services from some other company? Interacting with users who are real people? Built with a compiler running on a CPU you didn't design talking to other electronics that didn't exist when you proved your software?
I think I'd believe you have a time machine to sell me before I believe that your formal methods can work in messy real world.
The other white lie is that we can come up with a way to formally prove that the programmer can write perfect code through testing, licensing and certification. Programmers aren't plumbers. Plumbers deal with water, gases, pipes and valves. Like the bridge ingredients these things rarely change; after all fluid physics is a well known science and unlikely to spontaneously become something else.
I knew a guy who passed all the Java certifications yet when put on a real application was hopeless; he simply didn't get how to write a real body of code. Now imagine trying to certify someone in all programming languages, including ones not even invented yet! Add to that certification in every kind of program from toasters to spaceships. Either you create useless generic certifications or some that are so specific the certified are unemployable. Combine that with constantly changing needs for programmers and what do you do when you need something new, fire everyone you have and get all new people?
At work the UX designer and I are helping to mentor a group of Java web programmers in iOS development because we have more iOS needs than we have people. It's hard for even experienced programmers to do something radically different on the fly. Assuming we would need formal methodologists and certified iOS programmers to compete in our market we might as well close shop.
The new iPhone app we are developing with 3 of us (all experienced in iOS) in two months at a breakneck speed with constant changing requirements would not be possible unless we could actually deliver something fast enough to stave off the competition. Expecting some formal proof of all the code before shipping is a nightmare of a pipe dream. Who cares if it's certifiably perfect if it ships years after the company is gone.
Reality can certainly bite. Over the 30 years of real coding I have done I am confident what I have written is pretty good. During 1987-1994 I was responsible for writing (along with many others) and making the final decision on binaries delivered to a floppy disk duplicator for 11 major releases of 3 Mac applications and never once did we have to have a redo (Deltagraph alone cost nearly $1 million to duplicate and ship per release). Was the code perfect? Were we certified Mac OS C business/graphics programmers? No, and no. Were the applications useful and allowed people to do their business or whatever without too many irritations? Yes.
Does this prove anything? No. But good code is possible and does happen, and often from people with no license, degree, guarantee or formally proven skill.
Maybe someday a robot will write all software and prove it beyond any possible source of error and all humans will live happily in perfect software land.
Me, I'm betting on a time machine happening first. With software written by humans.