Right, that's optimization again. Basically the reason I'm asking about this is that I'm working on a theorem prover (with the intent of applying it to software verification), and if Alan Crowe considers current designs the wrong kind, I'm interested in ideas about what the right kind might be, and why. (The current state of the art does need to be extended, and I have some ideas of my own about to do that, but I'm sure there are things I'm missing.)