3 ms·

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

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...
- shasta 11y ago
  Actually, empirical observation depends on the correctness of basic logic, which must therefore precede it. You can't do experiments without having a logical framework that allows you to interpret their results. You can certainly find people who've convinced themselves that they need to empirically check math. i.e. check that 30x100 = 3x1000 by rearranging beans on their kitchen floor. I wouldn't hire anyone who did that to paint my bathroom, though.
  - mpweiher 11y ago
    That's the fallacy of uncritical rationalism. See Popper.
- asQuirreL 11y ago
  I prove mathematical properties purely for the sake of proving them. The fact that they have any bearing on the real world is a mildly interesting diversion. Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.
  - mpweiher 11y ago
    > I prove mathematical properties purely for the sake of proving them Good for you. I also think pure maths can be a fun diversion. > The fact that they have any bearing on the real world is a mildly interesting diversion. Well, computer "science" is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world. (And even if it were a "science", which it largely isn't, that would still be the case). > Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant always subsidiary to empirical evidence. > Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite. How do you know that while these proofs reference the infinite, they are actually applicable to the infinite? The answer is: you don't and you can't. You can only assume that the proof mechanisms you use actually do not break down. Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -> N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn't, what then? And of course, there always have been (and probably always will be) "proofs" that were later shown not to be correct, just like physical "laws" that turned out not to be laws. All knowledge is contingent, especially all-quantified knowledge. And I have to admit that I find the naive/rigid belief (it is no more than that) in the absolute power of proofs...charming :-)

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

shasta 11y ago
Actually, empirical observation depends on the correctness of basic logic, which must therefore precede it. You can't do experiments without having a logical framework that allows you to interpret their results. You can certainly find people who've convinced themselves that they need to empirically check math. i.e. check that 30x100 = 3x1000 by rearranging beans on their kitchen floor. I wouldn't hire anyone who did that to paint my bathroom, though.
- mpweiher 11y ago
  That's the fallacy of uncritical rationalism. See Popper.
asQuirreL 11y ago
I prove mathematical properties purely for the sake of proving them. The fact that they have any bearing on the real world is a mildly interesting diversion. Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.
- mpweiher 11y ago
  > I prove mathematical properties purely for the sake of proving them Good for you. I also think pure maths can be a fun diversion. > The fact that they have any bearing on the real world is a mildly interesting diversion. Well, computer "science" is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world. (And even if it were a "science", which it largely isn't, that would still be the case). > Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant always subsidiary to empirical evidence. > Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite. How do you know that while these proofs reference the infinite, they are actually applicable to the infinite? The answer is: you don't and you can't. You can only assume that the proof mechanisms you use actually do not break down. Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -> N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn't, what then? And of course, there always have been (and probably always will be) "proofs" that were later shown not to be correct, just like physical "laws" that turned out not to be laws. All knowledge is contingent, especially all-quantified knowledge. And I have to admit that I find the naive/rigid belief (it is no more than that) in the absolute power of proofs...charming :-)