Opinion on "loop invariants", and are these frequently used in the industry?

Question

I was thinking back to my freshman year at college (five years ago) when I took an exam to place-out of intro-level computer science. There was a question about loop invariants, and I was wondering if loop invariants are really necessary in this case or if the question was simply a bad example... the question was to write an iterative definition for a factorial function, and then to prove that the function was correct.

The code that I provided for the factorial function was as follows:

public static int factorial(int x)
{
     if ( x < 0 ){
         throw new IllegalArgumentException("Parameter must be >= 0");
     }else if ( x == 0 ){
         return 1;
     }else{
         int result = 1;
         for ( int i = 1; i <= x; i++ ){
             result*=i;
         }
         return result;
     }
}

My own proof of correctness was a proof by cases, and in each I asserted that it was correct by definition (x! is undefined for negative values, 0! is 1, and x! is 1*2*3...*x for a positive value of x). The professor wanted me to prove the loop using a loop invariant; however, my argument was that it was correct "by definition", because the definition of "x!" for a positive integer x is "the product of the integers from 1... x", and the for-loop in the else clause is simply a literal translation of this definition. Is a loop invariant really needed as a proof of correctness in this case? How complicated must a loop be before a loop invariant (and proper initialization and termination conditions) become necessary for a proof of correctness?

Additionally, I was wondering... how often are such formal proofs used in the industry? I have found that about half of my courses are very theoretical and proof-heavy and about half are very implementation and coding-heavy, without any formal or theoretical material. How much do these overlap in practice? If you do use proofs in the industry, when do you apply them (always, only if it's complicated, rarely, never)?

Edit
If we, ourselves, are convinced that a piece of code is correct, can convince others (informally) that it is correct, and there are unit tests in place, to what extent are formal proofs of correctness needed?

Answer 1

The professor wanted me to prove the loop using a loop invariant;

Your professor wanted to make sure you understood loop invariants, not just prove something about a very simple function.

Is a loop invariant really needed as a proof of correctness in this case?

Well, technically, no. By that reasoning, you don't need to write a factorial function, either: just use a library function! But that's not the point of the exercise.

How complicated must a loop be before a loop invariant (and proper initialization and termination conditions) become necessary for a proof of correctness?

I know some smart people who can probably prove just about anything without invariants, and then there's people who need to use them even for trivial cases like the above. That's like asking "how heavy does a rock have to be before you need a wheelbarrow to move it?".

Additionally, I was wondering... how often are such formal proofs used in the industry?

Written out explicitly? Probably rarely, unless you're in certain industries. But I still think about them when writing any but the most simple loop.

It's kind of like how I don't diagram sentences, but that doesn't mean I never think about grammar, especially if I'm writing some text that's really important. I can tell you what my pronoun's antecedent is, even though I'd never bother to put that fact on paper.