4 ms·

If that Haskeller you're referring to was me then I'd like to clarify: I think mathematics is a good fit for humans because it's the output of a few centuries o

by tel 11y ago

If that Haskeller you're referring to was me then I'd like to clarify: I think mathematics is a good fit for humans because it's the output of a few centuries of careful large scale use and design, not because it's simpler by any direct merit. Human languages might then be said to be the process of an even longer historical evolutionary process—so they must be the best, right? My thoughts here are that the natural selection pressures of human languages are very different than that of mathematical languages and we should direct the conversation there. Mathematics expresses a desire for (a) elegance and (b) economy of proof which might be taken to be an expression of the complete logic of a complex idea. This isn't the perfect thing to optimize for, but I think it's well in-line with what we're doing in programming. So I tend to take the bet that in the long run PLs and mathematics will converge and PLs will have further to move than the bulk of modern mathematical literature.

pron 11y ago
No, it wasn't you :) 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.
- tel 11y ago
  Well, phew! ;) 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.
  - pron 11y ago
    > 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)
    - tel 11y ago
      The bet is on, then, I suppose :) 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.

by tel 11y ago

pron 11y ago

No, it wasn't you :) 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.

tel 11y ago
Well, phew! ;) 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.
- pron 11y ago
  > 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)
  - tel 11y ago
    The bet is on, then, I suppose :) 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.