Hoare logic and proof-carrying code are two independent frameworks for
reasoning that programs meet their specifications. In this paper, we
merge the two approaches by embedding axiomatic specifications in a
type system for foundational proof-carrying code. By annotating
programs with proof hints, proof checking of Hoare triples becomes
decidable and as efficient as type checking.