We found that backtracking was basically useless in practice for RedPRL, because the state space would just blow up. I'm thinking that it actually may be a bad idea, and that in cases where we think we need backtracking, what we really need is to redesign the proof theory.