Theories and calculi for refinement of imperative programs have usually been fairly vague about the underlying logical basis. My talk describes some lessons learned from trying to formalise the whole of the Refinement Calculus inside higher order logic. These include a lattice-oriented formulation of the logic itself, a refinement-oriented proof format and some extensions to the Window Inference style of reasoning.