5 ms·

Oh yes it is. Programming is exactly equivalent to writing mathematical proofs. http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_isomorphism http://en.wikiped

by zeteo 14y ago

Oh yes it is. Programming is exactly equivalent to writing mathematical proofs. http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_isomorphism http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_isomorphis...

lincolnq 14y ago
Did you even read the article? Edit: This is exactly what the author is arguing against. Yes, you're writing a proof, but that's not the point of what you're doing at all.
- zeteo 14y ago
  Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Howard beg to differ.
  - ArtB 14y ago
    They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.
    - zeteo 14y ago
      Math went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.
  - scott_s 14y ago
    Most interesting programs cannot be studied analytically.
    - cantankerous 14y ago
      That's a pretty strong statement. Care to provide some examples?
      - scott_s 14y ago
        You are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.
        cantankerous 14y ago
        Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).
- deltasquared 14y ago
  I read the article and disagree. Computer science is a discipline of applied mathematics. Saying that computer science is not mathematics because it involves real world complications, is like saying that experimental physics isn't physics because it is not done by theorists.
ColinWright 14y ago
I'm having a hard time seeing how you can come to that conclusion based on the article you reference. Certainly a mathematical proof can be written in a program-style formal language, and then that type of programming becomes equivalent to those types of proofs. However, programming in general is simply not like that, and programming in general does not, to me, seem to be anything like doing math. And since that's a very personal statement, let me add by way of context that I have a PhD in math, I have programmed for a living, and I have written computer verified proofs. It seems to me that most of the people who claim that "programming is math" (and there are many, but perhaps not as many as the OP is implying) have never actually done any math at an advanced level. I'd be happier saying that programming is a lot like doing word problems, where it's essential not only to get the right answer, but also to use the the right terms, with the right grammar, and in a limited amount of space. And it's pass/fail.
- zeteo 14y ago
  >programming in general does not, to me, seem to be anything like doing math. Hi Colin, can you substantiate that? PhD in CS here and I've done some pretty hardcore math in my academic life. After writing lots of proofs and lots of programs the two activities don't seem that dissimilar. They are very different "programming languages" indeed, but debugging, modularity, recursion are important for both activities. To give a more concrete example: for my thesis I've implemented at one point a geometric algorithm. Some of the computer code proved buggy so I went to the white board and simply increased the complexity of the math formulas, which allowed me to write less code. I don't see an immense difference between this and, say, combining C and Python code in the same project.
  - ColinWright 14y ago
    >> programming in general does not, to me, >> seem to be anything like doing math. > Hi Colin, can you substantiate that? It's a statement about what I feel. As I say, I have a PhD in math (Pure Math: Graph Theory and Combinatorics). I have written many, many programs (both for money and not for money, both for myself and for others.) Coming up with proofs of things believed true but not yet proven does not feel to me to be at all, in any way, like programming. > After writing lots of proofs ... What sorts of proofs? Are these proofs of theorems, or are they calculations of formulas? > I went to the white board and simply increased > the complexity of the math formulas This feels to me like you are using "doing math" in a similar way to the way that someone "uses math" when adding up the grocery bill or dividing a restaurant check (but obviously insanely more complicated). I, too, have frequently stepped to the whiteboard to make more complex calculations, or derive more complex formulas, in order to simplify computations that must be done. That's not what I call "doing math." As I say, programming feels more to me like solving word problems, and I suspect that most of the divide and argument around this topic is caused by a lack of precision in the definition of "doing math". Which is ironic. Edits have been made for clarity.
jahewson 14y ago
No, no, no. The Curry-Howard Isomorphism applies to functional programming languages only.
- gatlin 14y ago
  And if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold for all Turing complete languages.
  - jahewson 14y ago
    Nope. C-H concerns the simply typed lambda calculus which is not Turing-complete. Thus C-H only applies to non-recursive functional programs (or equivalent). A proof is a program, but a program is not always a proof (as proofs must terminate).
    - gatlin 14y ago
      I concede. Thanks for the interesting tangent of reading that brought on, too!

by zeteo 14y ago

lincolnq 14y ago

Did you even read the article? Edit: This is exactly what the author is arguing against. Yes, you're writing a proof, but that's not the point of what you're doing at all.

zeteo 14y ago
Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Howard beg to differ.
- ArtB 14y ago
  They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.
  - zeteo 14y ago
    Math went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.
- scott_s 14y ago
  Most interesting programs cannot be studied analytically.
  - cantankerous 14y ago
    That's a pretty strong statement. Care to provide some examples?
    - scott_s 14y ago
      You are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.
      - cantankerous 14y ago
        Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).
deltasquared 14y ago
I read the article and disagree. Computer science is a discipline of applied mathematics. Saying that computer science is not mathematics because it involves real world complications, is like saying that experimental physics isn't physics because it is not done by theorists.

ColinWright 14y ago

I'm having a hard time seeing how you can come to that conclusion based on the article you reference. Certainly a mathematical proof can be written in a program-style formal language, and then that type of programming becomes equivalent to those types of proofs. However, programming in general is simply not like that, and programming in general does not, to me, seem to be anything like doing math. And since that's a very personal statement, let me add by way of context that I have a PhD in math, I have programmed for a living, and I have written computer verified proofs. It seems to me that most of the people who claim that "programming is math" (and there are many, but perhaps not as many as the OP is implying) have never actually done any math at an advanced level. I'd be happier saying that programming is a lot like doing word problems, where it's essential not only to get the right answer, but also to use the the right terms, with the right grammar, and in a limited amount of space. And it's pass/fail.

zeteo 14y ago
>programming in general does not, to me, seem to be anything like doing math. Hi Colin, can you substantiate that? PhD in CS here and I've done some pretty hardcore math in my academic life. After writing lots of proofs and lots of programs the two activities don't seem that dissimilar. They are very different "programming languages" indeed, but debugging, modularity, recursion are important for both activities. To give a more concrete example: for my thesis I've implemented at one point a geometric algorithm. Some of the computer code proved buggy so I went to the white board and simply increased the complexity of the math formulas, which allowed me to write less code. I don't see an immense difference between this and, say, combining C and Python code in the same project.
- ColinWright 14y ago
  >> programming in general does not, to me, >> seem to be anything like doing math. > Hi Colin, can you substantiate that? It's a statement about what I feel. As I say, I have a PhD in math (Pure Math: Graph Theory and Combinatorics). I have written many, many programs (both for money and not for money, both for myself and for others.) Coming up with proofs of things believed true but not yet proven does not feel to me to be at all, in any way, like programming. > After writing lots of proofs ... What sorts of proofs? Are these proofs of theorems, or are they calculations of formulas? > I went to the white board and simply increased > the complexity of the math formulas This feels to me like you are using "doing math" in a similar way to the way that someone "uses math" when adding up the grocery bill or dividing a restaurant check (but obviously insanely more complicated). I, too, have frequently stepped to the whiteboard to make more complex calculations, or derive more complex formulas, in order to simplify computations that must be done. That's not what I call "doing math." As I say, programming feels more to me like solving word problems, and I suspect that most of the divide and argument around this topic is caused by a lack of precision in the definition of "doing math". Which is ironic. Edits have been made for clarity.

jahewson 14y ago

No, no, no. The Curry-Howard Isomorphism applies to functional programming languages only.

gatlin 14y ago
And if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold for all Turing complete languages.
- jahewson 14y ago
  Nope. C-H concerns the simply typed lambda calculus which is not Turing-complete. Thus C-H only applies to non-recursive functional programs (or equivalent). A proof is a program, but a program is not always a proof (as proofs must terminate).
  - gatlin 14y ago
    I concede. Thanks for the interesting tangent of reading that brought on, too!