I have two issues with your argument. The first is the (implied, I think) assumption that C-H is the only way to apply math to programming languages. 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.
The second is the assumption that by virtue of being well-studied an academic field would somehow prove a good fit with human psychology. That demands some empirical results which, again, are so far very disappointing.
> So I tend to take the bet that in the long run PLs and mathematics will converge
If by that you mean that the C-H approach will win, I'm happy to take that bet.
I believe that over the past 15 years, the relative usage of Haskell by developers has only decreased (the number of people using Haskell has grown less than the total growth in the number of programmers, much due to JavaScript and the web), and even though I could be wrong about that (I basically made it up :)), it's not too far from the truth.
Don't get me wrong, there are certainly academic influences (coming from C-H languages) on mainstream, or hopefully-mainstream languages (Rust is a clear example), but I don't see any signs of a trend towards adopting C-H as a basic language design philosophy.
Other approaches say, we'll let people write code however they feel most comfortable doing (more or less), using types whose expressivity is defined not by the limits of the verifier but only by various concerns over language complexity, mental overhead, performance and teamwork, while we let the verifier prove whatever types it can. If it proves that the variable x is of type "an integer which is always equal to the current time in seconds modulo seven, except on Saturdays when it's always zero", then that's great!
I think there are workflow and ux efficiencies for having the compiler reject programs which are poorly typed. This typing can arise from either internal or external verifications for all I care, but the ergonomics of each vary a lot as well.
I think for both practical and ergonomic reasons, completely automated proofs are weak. There's no reason not to run them if you agree with the validity and importance of the theorem they represent, but by their nature the meaning and effectiveness is highly limited.
By having your proving language align with your programming language you sidestep this issue by forcing everyone's hand into revealing their intentions to the verifier. From a process perspective, this keeps people from cheating ("whip and bondage and all that") and it also, more imprtantly encourages the code author to tell a complete story of what they're doing instead of merely creating the artifact. This is great for the more "conversational" style of proving that occurs with things like Agda, Coq, Epigram.
External proofs can act similarly but I think your examples are often really archaic. It seems to me that I nteresting theorems must be derived alongside your program be they internal or external. JonPRL is an interesting demonstration of this method (as is NuPRL, but you can't really access that one).
To the first point: I'm happy to generalize my claim outside of merely C-H school (which I'd call the "logical" school, maybe this is the same or maybe it's more broad than what you mean by C-H) and make a mere subclaim that the logical school will prevail.
To the second point: I think there's plenty of existing empirical results, but not direct ones. E.g., how many advanced physicists today are using their own, highly divergent language for writing their theories (not their code, notably).
I think the direct empirical results—like the one you claim and I'd, without verification, buy—are conflated with technological progress and desire to get things done over getting them done consistently or well.
I'm not entirely sure what you mean, but if you mean that programmers will write code in languages that are directly tied to logical proofs (through the type system), then I'll take that bet.
> E.g., how many advanced physicists today are using their own, highly divergent language for writing their theories (not their code, notably).
Writing programs is not (or no longer) a scientific endeavor. I think software development is much more similar to the work of an architect. Some crucial parts can and must be verified sufficiently, others may have different MTBF requirements, other aspects are just aesthetic, very often you need to cut corners to meet budget and time requirements, and above all, your approach must be pragmatic and take into consideration that the building will need to be maintained and renovated by people other than you -- people with varying qualifications -- long after you've moved on to other projects.
> desire to get things done over getting them done consistently or well.
Perhaps, but what makes you think this desire will change? (I don't think it should change, but that's a different issue)
I think your point about architecture versus science is a good thing to think about. On one end, I agree with everything you're saying. On the other end, I see that architecture only works due to a large set of bombproof civil engineering practices employed both in the past to lay down the principles of architecture and continuously to validate that the work of the architects won't kill anyone.
My understanding is that these people are crucial to the success of any architecture project.
So with that I might ask whether the foundations for CS have been laid and whether the built-in civil engineers we employ are sufficiently able to do their jobs.
There is an immediate question as to whether we should care... and I'll just wave that aside for the moment since I have as least an aesthetic horse in the race that we should care.
After that we might ask if the founders of modern CS have done a sufficient job laying their foundations so we can use them. I'd believe there is some significant debate about whether this is true (Dijkstra would argue we're not even close, is my guess).
I'm willing to put a little, conservative bet on the idea that even if the "founders" all agreed their work was done that they'd be wrong, too. I just think this field is too young.
> 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.
The type system of Haskell is far more interesting and powerful than that of Java, but I think you're overstating the difference. While Haskell's type system does allow you to do a few more things than just demonstrate restraints on your code (such as construct more expressive types and make use of type classes and polymorphism), at the end of the day the overwhelming utility of the type system is being able to more easily make guarantees about your code, just as it is in Java.
Curry-Howard only really becomes interesting once you have dependent types, and only becomes bullet-proof when your language is total. Haskell has neither property. The connection to C-H is something which might interest a large subset of Haskell programmers (who would likely take that interest into a study of Coq, Agda or Idris), but it has pretty much no bearing on the day-to-day usage of Haskell.
