Our talk is about work in progress on the problem of how to reason about the computational complexity of programs in programming logics. We discuss complexity measures on inductive classes of functions as a way to internalize results on ramified recursion. We mention work with Karl Crary on formalizing evaluation and complexity in Nuprl, and we discuss Benzinger's system for heuristically approximating the complexity of first-order functional programs in Nuprl.