In Floyd-Hoare logic, the most common formal system for reasoning about the correctness of computer programs, there is the while rule.

In words, if you have a guard clause (the expression in brackets in the while()), a variant function (an expression with discrete values that can be shown to decrease monotonically each time the loop runs, and always be positive), and a loop invariant (a logic statement that is always true before and after every time the loop runs), you can prove that the while loop will finish (because the variant function can't keep decreasing) and that eventually the guard clause will be false and the loop invariant be true.

Floyd-Hoare logic doesn't have rules for for loops or whatever constructs actual languages may have.

However, as other answers explain, for loops can always be written in terms of while loops. That means that they can be reasoned about, it just takes a little more work.

If your teacher had courses at university where he had to provide correctness proofs of his programs, he probably wrote programs using only while loops. I know I did. And once you are used to thinking in terms of guards and variant functions and loop invariants, they seem very natural. Overusing while loops is a habit you see with CS graduates, I had to learn to stop doing that in my first months as a professional developer.

Somewhere down the line, your teacher misremembered all this as "good programmers use while loops", whereas what really happens is more like "some CS graduates turn their correctness proof habits into practical programming habits".

In Floyd-Hoare logic, the most common formal system for reasoning about the correctness of computer programs, there is the while rule.

In words, if you have a guard clause (the expression in brackets in the while()), a variant function (an expression with discrete values that can be shown to decrease monotonically each time the loop runs, and always be positive), and a loop invariant (a logic statement that is always true before and after every time the loop runs), you can prove that the while loop will finish (because the variant function can't keep decreasing) and that eventually the guard clause will be false and the loop invariant be true.

Floyd-Hoare logic doesn't have rules for for loops or whatever constructs actual languages may have.

However, as other answers explain, for loops can always be written in terms of while loops. That means that they can be reasoned about, it just takes a little more work.

If your teacher had courses at university where he had to provide correctness proofs of his programs, he probably wrote programs using only while loops. I know I did. And once you are used to thinking in terms of guards and variant functions and loop invariants, they seem very natural. Overusing while loops is a habit you see with CS graduates, I had to learn to stop doing that in my first months as a professional developer.

Somewhere down the line, your teacher misremembered all this as "good programmers use while loops", whereas what really happens is more like "some CS graduates turn their correctness proof habits into practical programming habits".