7 ms·

>Are these proofs of theorems, or are they calculations or formulas? A calculation is a kind of proof, isn't it? Lots of papers contain theorems and lemmas of

by zeteo 14y ago

>Are these proofs of theorems, or are they calculations or formulas? A calculation is a kind of proof, isn't it? Lots of papers contain theorems and lemmas of the form "f(x) = g(x)". I don't think proving such a formula is the same as applying some well-known algorithm (grocery / restaurant bill).

ColinWright 14y ago
And there's the difference. I do not think a calculation is necessarily a proof, but some proofs are accomplished by calculations. Some papers may contain a proof that "f(x)=g(x)" and proceed to prove the result by calculation, but that's not the only kind of proof, and it's not the only kind of calculation. And doing the kind of calculation that's in the intersection is not then programming. Sometimes in the act of programming you will do some math, but doing the math is enabling the programming. Doing the programming is not doing the math. It's a separate activity and a separate skill. Of course the boundaries are blurred, but I've honestly seen people write a program to take data from a database, present it nicely on the screen, and then assert that programming is just math. I doubt you're claiming that, but I've seen it claimed, and I think it's not only wrong, but misleading, and demeaning to both subjects. Sometimes you will use math in programming, and sometimes you will use programming in math. That doesn't mean that either is the other. And now I'm going to be controversial. And in case anyone else is still reading, here's a theorem: Theorem: A prime number can be written as the sum of two squares if and only if it is of the form 4k+1 . Just as there are many ways to write a program to accomplish a given task, there are many proofs of this theorem. If you're a programmer, and you think that programming is just math, then you should be able to come up with a proof for that theorem. The reason this is controversial is that many mathematicians couldn't come up with a proof quickly either. Here's another: Theorem: A number N is prime if and only if (N-1)!+1 is a multiple of N. And finally, one from my own area: Given a graph G=(V,E), a proper coloring is an assignment c:V->{1..n} of integers to vertices such that for every edge (u,v) in E, c(u) != c(v). (In words, color the vertices so that the endpoints of an edge are always colored differently). The "Chromatic Function" of a graph takes the number colors and returns the number of proper colorings. Theorem: For every graph, the Chromatic Function of G is a polynomial. People say that a good programmer can pick up a new language and/or library quite quickly and become productive in fairly short order. Most of the comments on HN about hiring practices say that you shouldn't test for knowledge of language or libraries or frameworks, but for actual ability to get things done. If programming is math, and someone is a programmer, shouldn't they be able to prove these theorems? ======== Disclaimer: This is a stronger position than I'm actually willing to defend, but I'm interested to hear people's views. ADDED IN EDIT: I've spent way too long on this and have things I must do. I'll return later to check for any replies. I'll also get a HN_Notify email if you do reply. Or email me directly.
- zeteo 14y ago
  Not every programmer can write any program with equal ease, can we? It depends on your knowledge of available primitives: programming languages, libraries. One who knows OpenGL will have an easier time spinning a 3D model than another who parses log files for a living. Similarly, a graph theorist like yourself will find it easier to prove theorems of form 3. than the rest of us. (At least half of th. 2 seems easier though. Suppose N divides (N-1)!+1; none of 2...(N-1) divides (N-1)!+1; so none of 2...(N-1) divides N.) I guess the main confusing part about the Howard-Curry isomorphism is that the code / comment conventions are commonly reversed between proofs and programs. Programs show a sequence of actions, and may show machine state in the comments, e.g. ... x = x * f; //x now contains factorial(n) ... Proofs show state instead (i.e. the proposition that was proven so far), and may contain the operation in the comments: ... (x + y) ^ 2 = (x + y) * (x + y) Using the distributivity of addition: (x + y) ^ 2 = (x + y) * x + (x + y) * y ... In either case, you: - start with an initial state - choose a sequence of operations from an existing set - end up with a desired state If either your program or proof has bugs, there are certain initial states that will break some step in the operation sequence and cause an undesired final state.
  - ColinWright 14y ago
    I've not been able to study the link about Howard-Curry isomorphism, but it seems largely to be talking about writing proofs in code. That's not the point. There are people who program for a living who I expect can't do that, and I expect that because I believe there are people who program for a living who can't do math (yet). Work has taken me away and I can't reply at length. I'm trying to find a math equivalent of FizzBuzz. I still claim programming is not math, and math is not programming. Skills in each can help the other, but aren't necessary. Engaging in the activity of programming is not "doing math." I will return to this topic when I can - now is not a good time.

by zeteo 14y ago

ColinWright 14y ago

And there's the difference. I do not think a calculation is necessarily a proof, but some proofs are accomplished by calculations. Some papers may contain a proof that "f(x)=g(x)" and proceed to prove the result by calculation, but that's not the only kind of proof, and it's not the only kind of calculation. And doing the kind of calculation that's in the intersection is not then programming. Sometimes in the act of programming you will do some math, but doing the math is enabling the programming. Doing the programming is not doing the math. It's a separate activity and a separate skill. Of course the boundaries are blurred, but I've honestly seen people write a program to take data from a database, present it nicely on the screen, and then assert that programming is just math. I doubt you're claiming that, but I've seen it claimed, and I think it's not only wrong, but misleading, and demeaning to both subjects. Sometimes you will use math in programming, and sometimes you will use programming in math. That doesn't mean that either is the other. And now I'm going to be controversial. And in case anyone else is still reading, here's a theorem: Theorem: A prime number can be written as the sum of two squares if and only if it is of the form 4k+1 . Just as there are many ways to write a program to accomplish a given task, there are many proofs of this theorem. If you're a programmer, and you think that programming is just math, then you should be able to come up with a proof for that theorem. The reason this is controversial is that many mathematicians couldn't come up with a proof quickly either. Here's another: Theorem: A number N is prime if and only if (N-1)!+1 is a multiple of N. And finally, one from my own area: Given a graph G=(V,E), a proper coloring is an assignment c:V->{1..n} of integers to vertices such that for every edge (u,v) in E, c(u) != c(v). (In words, color the vertices so that the endpoints of an edge are always colored differently). The "Chromatic Function" of a graph takes the number colors and returns the number of proper colorings. Theorem: For every graph, the Chromatic Function of G is a polynomial. People say that a good programmer can pick up a new language and/or library quite quickly and become productive in fairly short order. Most of the comments on HN about hiring practices say that you shouldn't test for knowledge of language or libraries or frameworks, but for actual ability to get things done. If programming is math, and someone is a programmer, shouldn't they be able to prove these theorems? ======== Disclaimer: This is a stronger position than I'm actually willing to defend, but I'm interested to hear people's views. ADDED IN EDIT: I've spent way too long on this and have things I must do. I'll return later to check for any replies. I'll also get a HN_Notify email if you do reply. Or email me directly.

zeteo 14y ago
Not every programmer can write any program with equal ease, can we? It depends on your knowledge of available primitives: programming languages, libraries. One who knows OpenGL will have an easier time spinning a 3D model than another who parses log files for a living. Similarly, a graph theorist like yourself will find it easier to prove theorems of form 3. than the rest of us. (At least half of th. 2 seems easier though. Suppose N divides (N-1)!+1; none of 2...(N-1) divides (N-1)!+1; so none of 2...(N-1) divides N.) I guess the main confusing part about the Howard-Curry isomorphism is that the code / comment conventions are commonly reversed between proofs and programs. Programs show a sequence of actions, and may show machine state in the comments, e.g. ... x = x * f; //x now contains factorial(n) ... Proofs show state instead (i.e. the proposition that was proven so far), and may contain the operation in the comments: ... (x + y) ^ 2 = (x + y) * (x + y) Using the distributivity of addition: (x + y) ^ 2 = (x + y) * x + (x + y) * y ... In either case, you: - start with an initial state - choose a sequence of operations from an existing set - end up with a desired state If either your program or proof has bugs, there are certain initial states that will break some step in the operation sequence and cause an undesired final state.
- ColinWright 14y ago
  I've not been able to study the link about Howard-Curry isomorphism, but it seems largely to be talking about writing proofs in code. That's not the point. There are people who program for a living who I expect can't do that, and I expect that because I believe there are people who program for a living who can't do math (yet). Work has taken me away and I can't reply at length. I'm trying to find a math equivalent of FizzBuzz. I still claim programming is not math, and math is not programming. Skills in each can help the other, but aren't necessary. Engaging in the activity of programming is not "doing math." I will return to this topic when I can - now is not a good time.