When Step Five Fails, Undo Steps One Through Four

The previous articles built up a picture of what a compiler can verify about individual operations:...