I'm not sure I can follow you here. What is ugly, Hoare logic? What does it mean to "build a whole language around Hoare logic"? What in your opinion are the alternatives to Hoare-style program logics that are general-purpose enough to work for arbitrary programming languages?