It's not really nonsense, it fits a common notion of entropy: lack of order or predictability; gradual decline into disorder.
As software systems (like many systems) go from initial development (which may or may not have a solid vision and initially highly disciplined development approach) to long term maintenance, disorder creeps into the system. Often just as a matter of expedience, "Let me make this field public so this other module can modify it directly because I need it now, I'll come up with a proper interface later. Oh shit, three years later 100 modules are making use of that public field."
What tests do, in this case, is help to preserve order. They help to ensure that a more rigid and ordered structure for the code remains. Formal methods only take you so far because, outside of maybe coq and related languages, there is no direct connection between your formal method spec and the code that has been written, in contrast to tests (which can be derived from your formal spec, but usually manually). Of course, tests can only carry you so far, they also have to be maintained. If a test is removed because it's no longer relevant, is another test put in its place to verify the new system? Are tests disabled because they're only failing sporadically or because the bugs they represent are hard to fix and we don't know how to yet (or don't have the time)?
Gradually, a system starts to suffer from various problems of this sort, that's entropy. Maintaining quality is a constant struggle against various forces (convenience, loss of institutional knowledge, time pressure, etc.). Tests are one way (and a critical way) to help balance against those forces.
EDIT: Other formal methods that work with real systems would be in Ada/SPARK, ATS, or Frama-C and I'm surprised I didn't mention them above. However, at least with SPARK, it narrows the scope of what you can do with the system and prove properties about it. That scope is always increasing, but is still a subset of what Ada itself can do. That's not all bad, but this means you can only consistently prove (in a formal sense) properties of subsets of a larger system and will likely be unable to prove (in an automatic fashion at least) a significant number of properties of those same larger systems.
