the dream of formalizing all reasoning has turned out to be a pipe-dream, as evidenced for example by the failure of the Hilbert program, and people everywhere proceed about their business as usual.
Ugh, that is unbelievably smug and disconnected from reality.
I could post tomes on why you are wrong. I will be kind and request you to respond to just this. :)
Automated reasoners have been quite useful. You just have to stop being so smug and start looking.
Your complaining is like the physicists ("natural philosophers"?) at Newton's time complaining that natural philosophy (physics) does not need all that weird math and normal language is enough for physics.
Do you understand the difference between "formalizing all reasoning" and just formalizing something?
Thanks for the condescending tone. But, you need to start somewhere. Be realistic.
Are you sitting and complaining that since physicists don't have a theory of everything already they should stop their work? Are you sitting and complaining that since we have not yet gone to Mars, NASA should be shut down? Are you also complaining that since we don't understand the genome fully, we should stop computational biology?
We start with approximations and we need to start small. Like in any science. Claiming reasoning is unformalizable is appealing to superstition and folk science.
And I was responding to the point that formalization has zero real world impact. That is patently false and intentional middle-brow FUD. This FUD can cause real harm to real people (not just people who study formal methods.)
You still have not responded to my example of formal methods being used in the real world with real impact.
I didn't claim anywhere formal methods are worthless or have zero real world impact. I said that the dream of formalizing all reasoning turned out to be a pipe-dream, and it did, as in:
Is that superstition and folk science? I also don't see mathematicians using mathematical logic to prove theorems in "ordinary" mathematics, hence the comment about "business as usual". I know formal methods are an active research field and successfully used in specialized applications in CS, but the article we are commenting upon is claiming studying formal methods is the best way to learn programming, which is similar to saying learning mathematical logic is the best way to learn mathematics, which is non-sense as evidenced by the attempts to do this.
People are even making money using formal reasoning. So please, take time to learn more before disparaging entire fields.
Btw, I know about the incompleteness theorems. I teach a course centered around that.
Let me ask you a related question: do you stop programming because many of the tasks associated with programming are Turing-uncomputable? (checking if a program halts, checking if two programs compute the same function etc.)
Comments
Ugh, that is unbelievably smug and disconnected from reality.
I could post tomes on why you are wrong. I will be kind and request you to respond to just this. :)
http://www.nytimes.com/library/cyber/week/1210math.html
Automated reasoners have been quite useful. You just have to stop being so smug and start looking.
Your complaining is like the physicists ("natural philosophers"?) at Newton's time complaining that natural philosophy (physics) does not need all that weird math and normal language is enough for physics.
Do you understand the difference between "formalizing all reasoning" and just formalizing something?
Thanks for the condescending tone. But, you need to start somewhere. Be realistic.
Are you sitting and complaining that since physicists don't have a theory of everything already they should stop their work? Are you sitting and complaining that since we have not yet gone to Mars, NASA should be shut down? Are you also complaining that since we don't understand the genome fully, we should stop computational biology?
We start with approximations and we need to start small. Like in any science. Claiming reasoning is unformalizable is appealing to superstition and folk science.
And I was responding to the point that formalization has zero real world impact. That is patently false and intentional middle-brow FUD. This FUD can cause real harm to real people (not just people who study formal methods.)
You still have not responded to my example of formal methods being used in the real world with real impact.
I didn't claim anywhere formal methods are worthless or have zero real world impact. I said that the dream of formalizing all reasoning turned out to be a pipe-dream, and it did, as in:
http://en.wikipedia.org/wiki/Hilbert%27s_program#G.C3.B6del....
Is that superstition and folk science? I also don't see mathematicians using mathematical logic to prove theorems in "ordinary" mathematics, hence the comment about "business as usual". I know formal methods are an active research field and successfully used in specialized applications in CS, but the article we are commenting upon is claiming studying formal methods is the best way to learn programming, which is similar to saying learning mathematical logic is the best way to learn mathematics, which is non-sense as evidenced by the attempts to do this.
You don't know does not equal to that not existing.
http://www.cs.miami.edu/~tptp/OverviewOfATP.html
People are even making money using formal reasoning. So please, take time to learn more before disparaging entire fields.
Btw, I know about the incompleteness theorems. I teach a course centered around that.
Let me ask you a related question: do you stop programming because many of the tasks associated with programming are Turing-uncomputable? (checking if a program halts, checking if two programs compute the same function etc.)