I'm still unclear about this, should this be done by the typing system or by an external static verifier:

   simple inductive proofs to show 
   that as you initialize 
   another element and add 1 to 
   the counter

If the latter, you can already do this with Rust as it is, it's just a question of building such a static verifier. If the former, I really doubt that this can fit in Rust's typing system without major surgery. We know well how to add arithmetic to typing systems, but the natural approach to doing so (dependent types) will probably make type-checking / -inference undecidable.