[neel_k]

Gap buffers are zippers, which makes this particular case really easy: they arise as derivatives of the list functor, and so for generic categorical reasons they are isomorphic to a list plus a position in it. This means you can prove things about lists-with-positions and basically automatically transport them to statements about gap buffers.

The specification in this note is not an ideal top-level spec, though: it just says there are a series of editor commands that can change one string into another. This is just a basic sanity check, but you can't do much more than that here because the editor state is too impoverished -- it's just the current string.

However, there is an interesting line of attack in (1) enriching the state enough to easily model richer things like command history and undo (eg, by making the state be the whole history of documents and commands), (2) giving each update command a semantics in terms of simple whole-state changes on the enriched state, and then (3) showing that a more efficient representation correctly implements the simple whole-state semantics.

About five years ago, Conor McBride taught a course on dependently-typed programming in Agda in which one of the projects was implementing provably correct text editors, using zippers/gap buffers and interaction via Mealy machines. The link is: https://github.com/pigworker/CS410-15