| It was me[1] and I'm afraid you are still mistaken on a number of points: > The truth is that Haskell -- like all programming language -- has made a design choice, which was to bake in correctness proofs based on the Curry-Howard correspondence into the language Haskell is not a logic and is not used to write proofs for program verification. General-purpose functional languages don't have all that much to do with CH, and they don't include any design decisions that favors a particular approach to verification. 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. > I think C-H has so far disappointed, because 1., people don't seem to want it, and 2. because other verification systems (like KeY) or the verifiable imperative, reactive real-time languages of the eighties (like Esterel) whose descendants are still in use today, have so far been used to much better effect. Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification. So, different tools for a different purpose. Having said that, they have proven to be very useful for verification of complex systems like those you listed, where existing tools have trouble even stating what correctness means. That is, they can help us answer the question "how can we be certain that this compiler, verification system, etc. is correct?" That typically includes representing your object language in your theorem prover and proving things about the language, which is quite different than showing that an algorithm meets some specification. > But the notion of subset => simpler is a mathematical notion with no relevance to cognition. If humans operated in this way, natural languages would have been much more mathematically simpler, too. 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. So, if you come to some correct conclusion, even if the way you reason is completely bogus and just happens to work, it will be valid for your simpler language. There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans". That's not to say that the current crop of functional languages is presented in the easiest way for people to understand, but that's an entirely different problem independent of semantic considerations. [1] https://www.reddit.com/r/programming/comments/3i1l9n/from_im... |
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.