9 ms·

Proofs are programs. https://www.google.com/search?q=proofs+are+programs https://www.google.com/search?q=proofs+are+programs

ekianjo 14y ago
Let me say it in another way. Abstract Maths is like having a Organic Chemist working on understanding the transformation of food at the molecular level. A Software Programmer is like a cook who knows how to mix and prepare food in order to make a delicious dish out of it.
- fusiongyro 14y ago
  "Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians."– E. W. Dijkstra
  - tinco 14y ago
    Mr Dijkstra obviously did not code in Ruby.
    - jacques_chester 14y ago
      I'm confident he'd look on Ruby as an insult.
      - tinco 14y ago
        I am confident people might believe something they don't understand to be an insult..
        jacques_chester 14y ago
        I don't follow you.
        tinco 14y ago
        I was hinting ignorance might be the cause of your confident dismissal of Ruby :) @btilly: it seems as though that would be a correct assertion. @jacques_chester: I did not know that, does he have a piece on programming languages he found disconcerting? Did he prefer Church over Turing? I don't think programming languages can really go beyond being strictly mathematical though..
        jacques_chester 14y ago
        Ruby is probably the language I've written more code in than anything else. I quite like it; I find myself chafing in lots of other languages. My point is that Dijkstra was kinda big on programming-as-strict-mathematics; a loosey-goosey super flexible language like Ruby would not have met with his favour, IMO.
        btilly 14y ago
        I think that ignorance of Dijkstra may be the cause of your confident appraisal that he would have liked Ruby.
        jacques_chester 14y ago
        His wikiquotes page will give you a flavour of his thought: http://en.wikiquote.org/wiki/Edsger_W._Dijkstra http://en.wikiquote.org/wiki/Edsger_W._Dijkstra But especially "On the Cruelty of Really Teaching Computer Science". http://en.wikipedia.org/wiki/The_Cruelty_of_Really_Teaching_Computer_Science http://en.wikipedia.org/wiki/The_Cruelty_of_Really_Teaching_...
  - ekianjo 14y ago
    Both are difficult, but at least in programming you can rely on manipulating actual "elements" of information. There is some tangible part in it, while sometimes very remote in certain cases. Abstract Mathematics go into spaces of n dimensions and stuff that most programmers would not be able to comprehend, just like most human beings cannot without tremedous time and effort. I think it is a false debate to say that one discipline is poorer or more valuable than the other. We need both Mathematicians to advance the theories and Programmers to apply their learnings into the real world. Everyone has its place.
    - fusiongyro 14y ago
      I agree with the thrust of what you're saying (one discipline is not poorer or more valuable than the other) but I take exception to your "campus supremacist" tone. True, organic chemistry and cooking serve different needs, but the organic chemist can appreciate cooking while the cook cannot appreciate organic chemistry, and the same superset implication is present in your second analogy (that programmers cannot appreciate N-dimensional spaces). I'd be more worried about this attitude if I thought you had much comprehension of the overlap of these fields. To take your own example, many machine learning algorithms begin with N-dimensional spaces (you know, the kind programmers can't comprehend) and go from there—support vector machines are the obvious example ("a support vector machine constructs a hyperplane or set of hyperplanes in a high- or infinite-dimensional space"). But that's just the beginning; the Curry-Howard isomorphism shows that proofs and programs are the same thing. That theorem provers exist at all seems to undermine your original point. The category-extras package for Haskell, which is a set of abstract algebraic entities that, to my knowledge, are used exclusively for mathematical experimentation and not of any practical application at all. On the other side of the coin, the only practical applications of number theory have been in cryptography, and the big name there (RSA) is simply modular arithmetic combined with things we expect to be true about large primes. This level of math produces practically applicable results roughly every thirty to fifty years. It's wonderful when it happens, but the idea that mathematicians are consistently churning out theories of practical import is laughable. We do have people doing that, and we call them applied mathematicians and computer scientists. Are most programmers sufficiently mathematical? No—Dijkstra bemoaned this at great length. Does this mean that mathematicians are somehow a superset of programmers? Absolutely not. Let me be clear. I'm arguing with your tone and the implication behind your ham-handed analogies. What you've simply stated (we need both), I agree with.
  - tel 14y ago
    Dijkstra did a kind of programming distant from most of it today. If to him programming is a difficult branch of applied mathematics, then HN is a forum talking about how best to calculate your tip after dinner.
    - fusiongyro 14y ago
      You guys really are masters of specious analogies. Comparing the best of one field to the worst of another isn't a legitimate comparison and you know it.
- konceptz 14y ago
  This is not a good analogy. Many programmers have training in computability theory and understand some very discrete principles. Just because they may become entrenched in UX or some other facet of coding, does not mean they're just "hacking" stuff together in a pleasing way. "A Software Programmer is like a cook who has an undergraduate degree in Organic Chemistry." May be a more apt analogy.
jhales 14y ago
In theory - The reality is there is not a working compiler except for a few special cases.
walrus 14y ago
Not quite. Proofs, in practice, are not programs. They do not contain every detail, nor are they written in completely consistent language.

ekianjo 14y ago

Let me say it in another way. Abstract Maths is like having a Organic Chemist working on understanding the transformation of food at the molecular level. A Software Programmer is like a cook who knows how to mix and prepare food in order to make a delicious dish out of it.

fusiongyro 14y ago
"Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians."– E. W. Dijkstra
- tinco 14y ago
  Mr Dijkstra obviously did not code in Ruby.
  - jacques_chester 14y ago
    I'm confident he'd look on Ruby as an insult.
    - tinco 14y ago
      I am confident people might believe something they don't understand to be an insult..
      - jacques_chester 14y ago
        I don't follow you.
        tinco 14y ago
        I was hinting ignorance might be the cause of your confident dismissal of Ruby :) @btilly: it seems as though that would be a correct assertion. @jacques_chester: I did not know that, does he have a piece on programming languages he found disconcerting? Did he prefer Church over Turing? I don't think programming languages can really go beyond being strictly mathematical though..
        jacques_chester 14y ago
        Ruby is probably the language I've written more code in than anything else. I quite like it; I find myself chafing in lots of other languages. My point is that Dijkstra was kinda big on programming-as-strict-mathematics; a loosey-goosey super flexible language like Ruby would not have met with his favour, IMO.
        btilly 14y ago
        I think that ignorance of Dijkstra may be the cause of your confident appraisal that he would have liked Ruby.
        jacques_chester 14y ago
        His wikiquotes page will give you a flavour of his thought: http://en.wikiquote.org/wiki/Edsger_W._Dijkstra http://en.wikiquote.org/wiki/Edsger_W._Dijkstra But especially "On the Cruelty of Really Teaching Computer Science". http://en.wikipedia.org/wiki/The_Cruelty_of_Really_Teaching_Computer_Science http://en.wikipedia.org/wiki/The_Cruelty_of_Really_Teaching_...
- ekianjo 14y ago
  Both are difficult, but at least in programming you can rely on manipulating actual "elements" of information. There is some tangible part in it, while sometimes very remote in certain cases. Abstract Mathematics go into spaces of n dimensions and stuff that most programmers would not be able to comprehend, just like most human beings cannot without tremedous time and effort. I think it is a false debate to say that one discipline is poorer or more valuable than the other. We need both Mathematicians to advance the theories and Programmers to apply their learnings into the real world. Everyone has its place.
  - fusiongyro 14y ago
    I agree with the thrust of what you're saying (one discipline is not poorer or more valuable than the other) but I take exception to your "campus supremacist" tone. True, organic chemistry and cooking serve different needs, but the organic chemist can appreciate cooking while the cook cannot appreciate organic chemistry, and the same superset implication is present in your second analogy (that programmers cannot appreciate N-dimensional spaces). I'd be more worried about this attitude if I thought you had much comprehension of the overlap of these fields. To take your own example, many machine learning algorithms begin with N-dimensional spaces (you know, the kind programmers can't comprehend) and go from there—support vector machines are the obvious example ("a support vector machine constructs a hyperplane or set of hyperplanes in a high- or infinite-dimensional space"). But that's just the beginning; the Curry-Howard isomorphism shows that proofs and programs are the same thing. That theorem provers exist at all seems to undermine your original point. The category-extras package for Haskell, which is a set of abstract algebraic entities that, to my knowledge, are used exclusively for mathematical experimentation and not of any practical application at all. On the other side of the coin, the only practical applications of number theory have been in cryptography, and the big name there (RSA) is simply modular arithmetic combined with things we expect to be true about large primes. This level of math produces practically applicable results roughly every thirty to fifty years. It's wonderful when it happens, but the idea that mathematicians are consistently churning out theories of practical import is laughable. We do have people doing that, and we call them applied mathematicians and computer scientists. Are most programmers sufficiently mathematical? No—Dijkstra bemoaned this at great length. Does this mean that mathematicians are somehow a superset of programmers? Absolutely not. Let me be clear. I'm arguing with your tone and the implication behind your ham-handed analogies. What you've simply stated (we need both), I agree with.
- tel 14y ago
  Dijkstra did a kind of programming distant from most of it today. If to him programming is a difficult branch of applied mathematics, then HN is a forum talking about how best to calculate your tip after dinner.
  - fusiongyro 14y ago
    You guys really are masters of specious analogies. Comparing the best of one field to the worst of another isn't a legitimate comparison and you know it.
konceptz 14y ago
This is not a good analogy. Many programmers have training in computability theory and understand some very discrete principles. Just because they may become entrenched in UX or some other facet of coding, does not mean they're just "hacking" stuff together in a pleasing way. "A Software Programmer is like a cook who has an undergraduate degree in Organic Chemistry." May be a more apt analogy.

jhales 14y ago

In theory - The reality is there is not a working compiler except for a few special cases.

walrus 14y ago

Not quite. Proofs, in practice, are not programs. They do not contain every detail, nor are they written in completely consistent language.