Comment Re:Some Math is Good (Score 1) 583
Yes, formal verification of non-trivial program has been done. The "industry usage" section of the Wikipedia article on formal verification for a few examples.
That said, it is currently extremely expensive because it requires skilled programmers spending a lot of time on the verification, so it is only done when the correctness of the program is very important. Making it cheap enough to be used in any significant proportion of software projects is indeed a pretty far off. Having a large, carefully considered test suite is much more tractable and generally considered good enough (the vast majority of software, in practice, does not need to be bug-free).
On the other hand, proving a specific algorithm (as opposed to an entire system) formally correct may require a lot less work and is often the only way to convince oneself that it is actually correct.
Also, I think the GP was talking about the formal thinking of mathematics in general carrying over to programming.