[eli_gottlieb]

>The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.

Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.

[pron]

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.

[mafribe]

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.

[mafribe]

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?