Harvey Friedman has done some nice work on leveraging his theory of explicit definitions for set theory (cf. [The Logical Strength of Mathematical Statements I][1], 1976) to give a language for doing mathamtics in a way that can be easily translated into proofs over ZFC.


  [1]: http://www.math.ohio-state.edu/~friedman/pdf/histLogStr1.pdf