Quick note: many of you are saying that this guy is totally out of touch with how math works, and that formal derivation of proofs is just fantasy. It's true that that's an extreme view, but it is in fact one that is held by some top mathematicians, even if a small minority. There are people who have built up research programs out of trying to make it a reality. See, for instance, Doron Zeilberger, who apparently describes himself as an "ultrafinitist":
A compiled computer program is certainly a rigorous description of something, God knows what, certainly not the programmer. This is just funny: "I think computer science has a tremendous amount to offer the fields of logic and mathematics. Specifically, I think that requiring all formulas to be executable by a finite, deterministic system (a computer program) could lead to a great increase in the level of rigor of th…
A compiled computer program is certainly a rigorous description of something, God knows what, certainly not the programmer. This is just funny: "I think computer science has a tremendous amount to offer the fields of logic and mathematics. Specifically, I think that requiring all formulas to be executable by a finite, deterministic system (a computer program) could lead to a great increase in the level of rigor of th…
What, with his comment about being able to eventually understand sociology using physics, I think this essay is easily 3 Cuil.
Quick note: many of you are saying that this guy is totally out of touch with how math works, and that formal derivation of proofs is just fantasy. It's true that that's an extreme view, but it is in fact one that is held by some top mathematicians, even if a small minority. There are people who have built up research programs out of trying to make it a reality. See, for instance, Doron Zeilberger, who apparently des…
I agree. The original post is echoing many of the views expressed at more length by Sussman and Wisdom in their book "Structure and Interpretation of Classical Mechanics." There they showed that a computational expression of classical mechanics was much more explicit and rigorous than the standard mathematical or physical treatments. They also have a similar long paper on differential geometry from a computational perspective:
http://groups.csail.mit.edu/mac/users/wisdom/AIM-2005-003.pd...
I think this guy has mathematics totally wrong. Maths just doesn't work today the way it did in Newton's time, and even back then people weren't satisfied with Newton's proofs, but they lacked an alternative so they had to use them anyway. If the author had his way, we would have refused to accept Newtonian physics for two centuries! Could you imagine the damage that would have done? > [A]ny realistic mathematical pr…
> Oh, and computer science papers never leave out trivial steps or assume domain knowledge?
That's irrelevant. The guy's argument is that computer programs don't leave out information: "If all this information isn't available in some form, the program simply will not work, as the interpreter/compiler will not know what to do with the program. This forces a certain intellectual honesty on the process of executing a program; nothing can be left unspecified."
Clearly, computer science papers are written by humans and will typically lack rigour, which has both advantages and disadvantages. Human communication can contain bullshit, but you can't bullshit a computer.
I think this guy has mathematics totally wrong. Maths just doesn't work today the way it did in Newton's time, and even back then people weren't satisfied with Newton's proofs, but they lacked an alternative so they had to use them anyway. If the author had his way, we would have refused to accept Newtonian physics for two centuries! Could you imagine the damage that would have done? > [A]ny realistic mathematical pr…
I think this guy just isn't too hot at mathematics. Omitting a trivial step (or domain specific knowledge) is not a lack of rigour, but a courtesy to the reader. The details can always be filled in cleanly. A very astute comment. In principle, mathematical proofs are supposed to be every bit as completely described as computer programs, but perhaps not as explicitly expressed. Edsger Dijkstra used to refer to mathema…
I'm not a mathematician, but I can imagine some sort of "library of derivation" whereupon, in order to prove something, say, based on arithmetic, you include (the language directive, not the verb) the specification of arithmetic derived in Principia Mathematica. Then the proving system follows your logic to its logic, and then to the logic they relied on, and so on, until everything is completely explicit. Basically, formal execution of bibliographies.
I think this guy has mathematics totally wrong. Maths just doesn't work today the way it did in Newton's time, and even back then people weren't satisfied with Newton's proofs, but they lacked an alternative so they had to use them anyway. If the author had his way, we would have refused to accept Newtonian physics for two centuries! Could you imagine the damage that would have done? > [A]ny realistic mathematical pr…
> Oh, and computer science papers never leave out trivial steps or assume domain knowledge? That's irrelevant. The guy's argument is that computer programs don't leave out information: "If all this information isn't available in some form, the program simply will not work, as the interpreter/compiler will not know what to do with the program. This forces a certain intellectual honesty on the process of executing a pr…
His conclusion is that computer science is more rigorous than mathematics. His argument is that programs written for computers are more explicit than proofs written for humans. The conclusion and the argument don't match up at all. Computer science, as a subject, is no more rigorous than mathematics.
Quick note: many of you are saying that this guy is totally out of touch with how math works, and that formal derivation of proofs is just fantasy. It's true that that's an extreme view, but it is in fact one that is held by some top mathematicians, even if a small minority. There are people who have built up research programs out of trying to make it a reality. See, for instance, Doron Zeilberger, who apparently des…
It's not the claim that mathematics sometimes lacks rigour that's bothering anyone. It's the claim that computer science, as a subject, is somehow more rigorous than mathematics. It's the false equivalence of programs with computer science that's wrong.
Quick note: many of you are saying that this guy is totally out of touch with how math works, and that formal derivation of proofs is just fantasy. It's true that that's an extreme view, but it is in fact one that is held by some top mathematicians, even if a small minority. There are people who have built up research programs out of trying to make it a reality. See, for instance, Doron Zeilberger, who apparently des…
I agree. The original post is echoing many of the views expressed at more length by Sussman and Wisdom in their book "Structure and Interpretation of Classical Mechanics." There they showed that a computational expression of classical mechanics was much more explicit and rigorous than the standard mathematical or physical treatments. They also have a similar long paper on differential geometry from a computational pe…
Their point in SICM was that traditional notation was not as ambiguous as their computational notation. That's because traditional notation is designed to be convenient rather than explicit. They are right, but this does not mean that physics lacks rigour. More explicit notations were always available and physicists, being more intelligent than computers, were capable of resolving the ambiguities to reveal the fully rigorous structure underneath.
There's a difference between using a convenient notation and lacking rigour. If you are always capable of discerning the true formal equations behind a convenient notation then everything is OK. If you can't, or people can't agree on what the formal meaning should be, then there is indeed a problem. The fact that the authors could derive a computational notation that no physicist would disagree with is proof that a lack of rigour never existed in the first place.