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.
> make a mere subclaim that the logical school will prevail.
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.
I thought about exactly that as I was writing the analogy, and I just don't know... :)
I do think, though, that just like with architecture, different components require different care, and those that require absolute correctness are a rather small part. I also think that math (as in architecture) is only a very small part of the solution. It's essential, but it doesn't dictate the path of the project, and in the end most of it is just a lot of knowledge of how people behave (the people who live or work in the building and the people who will run, clean and maintain it).
I do, however, believe in the combination of familiar "cognitive" languages alongside verification tools. For example, see how Amazon uses TLA+ to verify their Java programs[1]. This alone is more real-world usage than Haskell has ever seen.
I think you're pointing out the difference between the "art" and "science" of architecture. A similar thing arises, IMO, in technical products between product and technology. There's a whole hell of a lot of psychology on the product side, and I think there always will be. Constrained by some artificial line to the technology side, I take my bet that mathematical tendencies will dominate.
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.