You don't need to build a "whole language" around any kind of logic for it to be sufficiently verifiable. Types are useful, but it's not necessarily an all-or-nothing question. There are non-type-based verification tools (symbolic execution and deduction), and tests complete the picture. A language that doesn't let you write a program unless you yourself have worked hard to prove to the compiler that it's correct may be more trouble than it's worth. Verification does not necessarily have to be a part of compilation, and it does not necessarily require the proof to be spelled out in code.

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?