We show how a full-scale automated-reasoning engine implemented in Smalltalk can be applied to assist in the programmer’s cognitive task of traversing abstraction levels. This approach follows naturally from our definition of debugging as any activity aimed towards understanding a program. We introduce the notion of “dimensions of abstraction”, give two examples (“stratum” and “mode”), and show how it is applied in debugging a native compiler backend.