We establish a match between two broad approaches to reasoning about programs: modal (dynamic logic) proofs on the one hand, and explicit higher-order reference to program semantics, on the other. We show that Pratt-Segerberg?s firstorder dynamic logic DL proves precisely program properties that are provable in second-order logic with set-existence restricted to a natural class of formulas, well-known to be related to computation theory