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 agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to worry about correctness and termination from Day 1.

Moreover, Cury-Howard based approaches really work only for a restricted form of programming: pure and total functions.

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?