> It was me
Yes, it was you :)
> The type system helps you enforce useful invariants in your code and can make verification easier, but it's completely orthogonal to how you can prove programs correct.
That's true for Java. Haskell, OTOH, constructs the entire language around verification through types and pure functions, and everything else is secondary. I don't know if the connection to C-H was made later or was a conscious design decision, but the result is the same from the user's perspective.
> Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification
We've discussed this before, and I believe those uses are too niche for the Haskell approach to gain any significant traction.
> You can show that, quite literally, any "true property" of a program in your more complicated language is also true of the corresponding program in your simpler language.
Of course, but that is only useful if a human programmer writing in the more "complicated" (by your definition) language would use the "simpler" subset, which, by my definition, she wouldn't do.
> There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans".
It's not a mathematical problem with a clear solution, and therefore requires no robust specification -- just like architecture (of buildings), or any other UI design problem. We learn what works through trial and error and try to do better.
I find it hard to accept the point of view which considers UI to be a methematical puzzle, or, alternatively, that doesn't recognize programming languages as UIs.
> but that's an entirely different problem independent of semantic considerations.
From a UI design perspective, you can't separate the two, because if the user fails to interact with the machine well, you don't know if it's a matter of design or presentation unless you empirically test it.