For me, debugging or perhaps more appropriately anti-bugging a program is so much like proving a theorem that the difference is one of terminology and notation rather than essence.