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.
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.)
