I'm abit afraid to ask this question here seeing as I asked it on programmers SE already, the thing is I think the question is more about the underlying theory than the use in practice (or call it confirmation bias). (If people here agree i should not have asked it here I will delete it and offer my sincere apologies) however I do think it will get a deeper meaning here as to why this is or isn't true.Here is the question:I have a teacher who (to me) seems quite intelligent, he really knows what he is talking about but he said something which surprised me (I'm paraphrasing): while loops can be proven where as for loops cannot. I think this translates to: One can completely explain what happens in a while loop whereas you cannot do that for a for loopIs my teacher right? (maybe this was the case when he started learning? ) and a more subjective question: Is there any clear reasoning behind this (why he would have stated this)?
provability of while loop vs for loop
correctness proof;loops
In a nutshell: What your teacher probably meant is that the semantics of while is pretty much the same in most languages, while the semantics of for may change considerably (see discussion below). Hence, abstract language independent proof are more reliable with a while, but one should be careful that a proof with a for loop may not match the semantics of the for loop in many languages.Your question is not precise enough (though that may not be yourfault).The point is that, afaik, there is no official, ISO supportedstandard, or otherwise officially accepted reference definition offor and while loops. The definition depends on the programminglanguage.Hence you cannot make any general statement regarding theirequivalence before you have defined precisely what each can do. Iadress that more precisely, since it is one of the main argument usedin other answers (and the discussion will be useful in what follows).On intertranslatability of for and while loopsSummary: it depends on the programming language, but is alwayspossible a long as you can have one infinite loop and a way to get outof it.But you can make such a statement for a specific programming language,and the answer will depend on the features fo the language.That also means that there is no general proof, but only one for eachprogramming language.One thing that is generally true is that a while loop can generallymimic a for loop, because the while loop can do the exit conditiontesting of the for loop, doing the initialisation of the controlvariable with an assignment before entering the loop, and doing theincrementation at the end of the loop body, so thatfor i from 1 by 2 to 10 do { xxx }becomesi=1while i11 do { xxx; ii+2 }This more or less works for most languages, but it is not as obvious asit seem, and there may be many details to worry about.For example, in many languages, the for loop evaluates it 3arguments (initial value, increment, and final value) as strictarguments, evaluated once before entering the loop, while others willtake then as thunk arguments to be reevaluated at each turn, orpossibly as lazy argument to be evaluated only when first needed.Another point may be that the increment variable may be local to thefor loop, or have to be a local variable of the function where theloop appears.Depending on such issues, the translation of a for to a while mayvary widely, though it is usually possible to achieve it.The same holds for the converse, thranslating a while into a for loop.Th first problem is that a while loop will always reevaluate theexit condition at each turn. But some for loops do not provide for acondition that is reevaluated at each turn, other than comparison ofthe control variable with some fixed value computed on loop entry.Then the translation is not possible unless there is some other meanto jump out of the loop on some arbitrary conditions.That is achievable with various devices, usually starting with aconditional statement testing the condition, followed by an a jump outimplemented, as available, by a loop exit statement, a returnstatement (after encapsulating the loop in a function), a gotostatement or an exception raising.In other words, it is again very dependent on languages, and possiblyon subtle features of languages.This say, as answered by @milleniumbug, the intertranslation is easyin the language C, because a for lopp is essentially a while loopplus some extra for an incremented control variable.But this does not necessarily apply to other languages, and mostlikely not in the same way.This being said, programming languages are usually supposed to haveTuring power with only one of these loops, since all you need for itis one infinite loop. So, as long as you have some way of looping forever, and possibly deciding to stop, you are pretty sure you can mimicany other construct ... but not necessarily easily.Regarding proofsSummary: There is no reason known to me to assert that proofs should be significantly harder with one or the other (unless some weird feature of the language).There is probably a misunderstanding, or your teacher had his mind onsomething else.Formals semantics can be defined for the various kinds of loopsdefined in programming languages, and then used for provingproperties.It may be, again depending on the language, that conducting formalproofs regarding programs may be more complex in some cases. But thatdepends on the language.I cannot imagine a reason why proofs should be significantly harder with one construct more than with the other. The for loop may be more complex since it can offer, as in C, all that is done with a while plus other things. But if you did it with a while, you would have to add the extras in some other form.I could use the formal general argument of intertranslatability, as long as there is the possibility for a single infinite loop. I will however refrain from doing that, as the constructions involved are nothing you want to deal with in a proof, and it would clearly be an unfair statement, at least in practice.Following the above discussion, however, we have seen that the difficulties for intertranslatability come from the great variability of the for loop from language to language. Hence the following conclusion which is probably the right answer:One possibility to understand your teacher's statement is that the semantics of the while loop is pretty much the same in all programming languages, while the syntax and semantics of the for loop can vary significantly from language to language. Hence, it is possible to make general abstract proofs with while loops that have language independent semantics to a good extent, while this is not possible for the for loop that has syntax and semantics changing too much from language to language. But this does not apply within a given language, when the semantics of both are precisely defined.My best suggestion is that you should ask your teacher what he precisely meant, and whether he can give you an example. Misphrasing or misunderstanding is a common event.