I had thought this was going to be about formal methods. Some languages (like SPARK) allow you to formally prove properties of programs -- for example, that th

I had thought this was going to be about formal methods. Some languages (like SPARK) allow you to formally prove properties of programs -- for example, that they cannot have a run-time exception. Actually, formal methods would dovetail well with the article's #1 point, "Big Design Up Front": you can't prove anything interesting about the software unless you have a formal spec of what it should do.