This post is the third in a series of me trying to work out batches, a new data structure I am testing for Herbie and more generally for programming with recursive data structures. In my first post I laid out a type theory for batches, and in my second post I discussed how we can check that programs that use batches are safe. But I'm still after a "holy grail": how to making programming with batches "normal". Specifically, most programming with batches involves lots of indices, which need to ...
