[pron]

Most software is very different from one that drives cars, but even in that case, while a complete specification (i.e., one that fully describes what driving a car safely is) is very hard, you can still quite easily specify many very useful correctness conditions. For example, you could state that the car must never go on the sidewalk or move to oncoming traffic unless it's trying to avoid some accident; similarly for running a red light, going over a crosswalk while there are pedestrians on it, or going over 100MPH. Verifying each of those would make your program safer, and that's the goal of formal methods -- not to make the program perfect, but better.

A complete formal specification of simpler programs or program components -- say banking systems or specific controllers in the car -- are not only possible and feasible but actually used in practice. A good number (I don't know if it's the majority or not) of avionics programs are formally specified and verified (although normally using model checkers rather than proofs). Having said that, different kinds of software can benefit from formal methods to different degrees. I'd say that if you can write tests for it, then you can write at least partial specs for it, too, but whether or not doing so is worth it varies by circumstance (in the cases I've used formal methods recently, it was not for more correctness but actually because it was cheaper than tests).

Also, we must separate formal specification from formal proof. Formal specification means writing what the program must or must not do in some precise formal language. Formal proof is one of many forms of verifying that specification. It provides the most confidence, but it is also by far the most expensive. Most programs can benefit greatly from formal specifications but can settle for weaker, but far cheaper, forms of verifying them.