Largely orthogonal to your comment: One interesting thing I learned/realized when reading about the msr dafny project is that for loops mean you need to provid

Largely orthogonal to your comment: One interesting thing I learned/realized when reading about the msr dafny project is that for loops mean you need to provide guarantees about invariants. How do I know there's no index out of bounds? How do I know how large the resulting array is? When you have to write post conditions for each loop, it makes higher order functions (map, reduce, filter) much more appealing. The proof was already done in the function that will invoke yours!