5 ms·

Not the case. The same argument does not apply because of the nature of mathematical, and to a certain extent scientific. All three--mathematics, science, and c

Not the case. The same argument does not apply because of the nature of mathematical, and to a certain extent scientific. All three--mathematics, science, and computing (programming)--are similar in that their primary currency is knowledge that can be concisely described and embodied in instruments (tools), either of which can then be used by others without too much of a concern for where that knowledge or instrument came from as long as there's a good instruction manual nearby. The knowledge and instruments are used to create more knowledge, which is embodied in more instruments, and the cycle continues on and on etc. The difference between computing and mathematics is the form that the knowledge and the instruments take. In mathematics, the concepts you're dealing with (or inventing, since I'm not a mathematical realist) are very clean and they stack well. You also have virtually no instruments to speak of. As a mathematician, it's not too common that you reduce your theories to practice. That's something that's left to the lesser sciences, such as computing. In computing, the relationship between between knowledge and instruments is that of identity. At the very least, the two are conflated in casual discussion. More concretely, the "knowledge" of computing is typically a model of some problem domain and the the instruments are software, which in turn manipulate the physical world (that's what your JavaScript is doing) in order to perform some task or measurement in service of solving some problem in your domain. So in mathematics, you have no correspondence between knowledge and instruments to do deal with. In computing, that's all you're dealing with except people are only really interested in the knowledge as its embodiment in the instruments. Static typing ensures that some sliver of that knowledge is explicit and checked. It doesn't mean it corresponds to the thing in your brain, but it does ensure that whatever's written down is embodied in your code. Mathematicians have no such constraints to deal with. They would if the proofs that they wrote were formal proofs, but they're not. Most, if not all, mathematicians know this. Most programmers, though, don't.

mpweiher 11y ago
> Static typing ensures that some sliver of that knowledge is explicit and checked. No. Testing ensures that the knowledge is checked. As in: run experiments. Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don't get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence. In every other engineering discipline, math is seen as a tool, simulations are cost saving measure because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally cheaper than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment. If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation. Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- seliopou 11y ago
  First, > some sliver Second, I for the most part agree with you in the ways that are relevant to the point you're trying to make. However, the knowledge/tool distinction is a vague (in that they may fall on a spectrum) and ambiguous (both words tend to be moving targets), which is why I chose the term instrument instead. Mathematics is a tool only in the sense that it is knowledge that is applied towards some benefit, e.g., efficiency. Also, > Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it." This is again "proof" in the day-to-day mathematical sense of a convincing argument, not in the formal sense for writing down an expression per line such that each line can be logically deduced from some preceding lines through the the use of axioms. A type checker is literally a search procedure through the space of derivation trees to find a formal proof that this term has this type.
  - isolate 11y ago
    Type checking is a conservative analysis, and the type correctness of a program is undecidable. But you can still rely on the knowledge generated by your type checker without having to run your program. Among other things, this allows you to optimize your program automatically.
  - mpweiher 11y ago
    > "proof" in the day-to-day mathematical sense of a convincing argument IIRC, that is the most that a so-called "proof" can ever be. I remember reading Carl Friedrich von Weizsäcker's "Aufbau der Physik"[1] in my younger years, and being somewhat flabbergasted when he starts by justifying classical logic, which he needs to do because later he talks about quantum logic, which is different. Up to that point, it had never occurred to me to justify logic empirically, but now I can't imagine naively accepting it. That means that empirical evidence always trumps. Everything. If we find logical rules that we assume violated in the real world, we have to deal with it, not deny reality. Just like we had to accept that other aspects of the world we held as self-evident were not just theoretically contingent, but actually turned out not to be true. > not in the formal sense for writing down an expression per line > such that each line can be logically deduced from some preceding > lines through the the use of axioms. Hmm...that's how we always did (simple) mathematical proofs: line-by-line, with axioms or theorems justifying the transformation from line to line. Last time I checked, so-called "machine-proofs" are definitely seen as different by mathematicians, yes, but they are less well-respected, not more so. Has this changed? [1] http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker/dp/3423330848 http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker...

mpweiher 11y ago

> Static typing ensures that some sliver of that knowledge is explicit and checked. No. Testing ensures that the knowledge is checked. As in: run experiments. Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don't get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence. In every other engineering discipline, math is seen as a tool, simulations are cost saving measure because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally cheaper than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment. If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation. Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

seliopou 11y ago
First, > some sliver Second, I for the most part agree with you in the ways that are relevant to the point you're trying to make. However, the knowledge/tool distinction is a vague (in that they may fall on a spectrum) and ambiguous (both words tend to be moving targets), which is why I chose the term instrument instead. Mathematics is a tool only in the sense that it is knowledge that is applied towards some benefit, e.g., efficiency. Also, > Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it." This is again "proof" in the day-to-day mathematical sense of a convincing argument, not in the formal sense for writing down an expression per line such that each line can be logically deduced from some preceding lines through the the use of axioms. A type checker is literally a search procedure through the space of derivation trees to find a formal proof that this term has this type.
- isolate 11y ago
  Type checking is a conservative analysis, and the type correctness of a program is undecidable. But you can still rely on the knowledge generated by your type checker without having to run your program. Among other things, this allows you to optimize your program automatically.
- mpweiher 11y ago
  > "proof" in the day-to-day mathematical sense of a convincing argument IIRC, that is the most that a so-called "proof" can ever be. I remember reading Carl Friedrich von Weizsäcker's "Aufbau der Physik"[1] in my younger years, and being somewhat flabbergasted when he starts by justifying classical logic, which he needs to do because later he talks about quantum logic, which is different. Up to that point, it had never occurred to me to justify logic empirically, but now I can't imagine naively accepting it. That means that empirical evidence always trumps. Everything. If we find logical rules that we assume violated in the real world, we have to deal with it, not deny reality. Just like we had to accept that other aspects of the world we held as self-evident were not just theoretically contingent, but actually turned out not to be true. > not in the formal sense for writing down an expression per line > such that each line can be logically deduced from some preceding > lines through the the use of axioms. Hmm...that's how we always did (simple) mathematical proofs: line-by-line, with axioms or theorems justifying the transformation from line to line. Last time I checked, so-called "machine-proofs" are definitely seen as different by mathematicians, yes, but they are less well-respected, not more so. Has this changed? [1] http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker/dp/3423330848 http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker...