The separation of implementation and algorithm, and the utility of formal specs and proofs. This roughly translates to machine assisted proofs and model checkin

The separation of implementation and algorithm, and the utility of formal specs and proofs. This roughly translates to machine assisted proofs and model checking. Namely, ACL2 and TLA+. I found these technologies and methods enormously beneficial to abstract thinking and producing good systems. Leslie Lamport, creator of TLA+ (and LaTeX), put out a lot of content about this topic and I was lucky enough to stumble upon it.