But sometimes the gap is wider. An only slightly more complex example would be "the shopping cart contains all items added to it in the current session and not subsequently removed". Sounds trivial, right? Well, as it happens, just a couple of days ago I bought two items from a site whose cart was broken -- it would show only the most recently added item. (I had to make two transactions. Fortunately no shipping fees were involved.) Okay, that's a rare sort of bug, but it just shows how even very simple invariants can get broken on occasion.
Sometimes the gap is even wider. "This app must have no XSS vulnerabilities." There's no one place in the program where you can see that that property is correctly implemented.
You see where I'm going with this: the wider the specification-implementation gap, the more useful formal methods can be.
And in saying that, I see that I was probably unfair to haskellandchill's point. The claim wasn't that I needed set theory; the claim was that the tools needed it (at least, so it appears to me on re-reading).
That being said, hopefully you won't have to use set theory, where any structure that actually matters to you has to be encoded in terms of sets containing sets containing sets, until you reach turtles.