Proof techniques for string algorithms? I'm currently reading through the tome "Algorithms on Strings, Trees, and Sequences" by Dan Gusfield, and I find the proofs to be extremely case analysis heavy and full of finicky +-1s. This seems very error prone to program. 

I was hoping for a more "conceptual" way to build string algorithms, where we first construct a toolkit of basic objects that we then use. I was hoping that prefixes, suffixes, and the Z algorithm would be those. But they seem too level to construct something like Boyer-Moore or Aho-Corasick.

As an analogy for some kind of abstract algebraic flavoured approach, like using matroids for greedy algorithms to capture the "hard" part of the analysis.

So my question is, are there nice algebraic structures that govern string algorithms which can be used to present and implement them more elegantly?
There is some work on developing an algebraic or grammar-based view of string algorithms, for example

Robert Giegerich, Carsten Meyer, Peter Steffen:
A discipline of dynamic programming over sequence data. Sci. Comput. Program. 51(3): 215-263 (2004)

Robert Giegerich, Hélène Touzet:
Modeling Dynamic Programming Problems over Sequences and Trees with Inverse Coupled Rewrite Systems. Algorithms 7(1): 62-144 (2014)

These approaches deal with string problems that are solved by dynamic programming such as the computation of edit distance or local alignments or comparison of RNA secondary structures. These problems are more difficult in terms of the running time of the best algorithms than the exact pattern matching problem that is solved by Boyer-Moore. 

A more conceptual or programmer-friendly approach for exact pattern matching would be to use the right data structures such as suffix arrays or suffix trees. Many pattern matching algorithms become simpler when these data structures are used as a black box or augmented in some relatively easy way.