Formally Verifying Rust's Opaque Types (dylanj.xyz)

The closest thing to an argument I am making is that iterators are a different language construct than a basic looping construct. If you disagree that’s fine, like I said, I’m not trying to ‘win’ anything or convince anyone of anything.

Edit to refer to sibling comment — As I said in a sibling comment, the iterator loop construct is syntactic sugar and that’s why I was saying it is different from discussing a more basic looping construct.

I would have to check the intermediate language, but I assume the for in construct is implemented, at the semantic level as an iterator object inside a while or basic loop construct.

Edit — I just checked and docs.rust-langexplicitly states that the for in construct is ‘syntactic sugar’ for the common case of looping over a container that implements the iterator trait.

    for i in 1..n {
        some_mut_arr[i] = T::default();
    }

    // OR
    mut i = 0;
    while i < n {
        do_something(some_arr[i]);
        i += 1;
    }

I don't disagree that the translation may result in roughly similar assembly/bytecode instructions in many languages, and while TFA is Rust-centric and most of the conversation has been too, my issues with iterators are not restricted to Rust. Further, my objection to using them in my own code is not strictly a performance issue (although, I am never in favor of coding and hoping it gets optimized).

Inherently, iterators are a more complex concept than a loop (or the tail recursive equivalent). Iterators are an object in and of themselves that are by design more complex than a natural number index, then you still need the actual looping construct. I am aware there are reasons that iterators are preferred and often recommended in some situations. However, the determination to use an iterator based construct in your code is not a universal declaration of fitness, it is only a case-by-case determination weighed against whatever other factors matter to the people writing the code. I also think this applies to the pushing of iterators as an idiomatic construct in a programming language, i.e. whether iterators are idiomatic is a determination that is made by the language designers when weighed against the established goals and priorities of the language as a whole.

Regarding the iterator-based code enabling optimizations that make the resulting compiled code faster than a basic while loop: I will admit that there is a possibility for this to occur. However, that is tempered by an educated guess that the enabling of those optimizations only occur because the compiler writers have explicitly coded in a 'hot-path' for iterator constructs into the IR. Also, there is the chance that the compiler writers use the higher level IRs to memoize data about the loop as a whole (based on knowledge of the language's iterator construct) and the presence of that data at later stages of the compiler allow for optimizations to occur, whereas the while loop would not trigger the memoization steps and then could not produce the optimizations. Both of those circumstances are a result of the language designers/compiler writers basing code generation (or IR generation) off of the idioms of the language and the underlying semantic definitions of the language.

As an aside, I am not certain Rust's compiler treats iterators the way I described above, but I would be surprised if it was not.