3 ms·

>All those symbols you see map to a set of steps (a program.) Simply not true. Most mathematical statements, e.g. proofs of existence have no relation to a "pr

>All those symbols you see map to a set of steps (a program.) Simply not true. Most mathematical statements, e.g. proofs of existence have no relation to a "program". >math is geared and targeted for people who like doing symbolic logic by hand. No, it is not. There is absolutely nothing interesting about symbol manipulation, it is always the least interesting part of a proof. It usually is the part the author handwaves away, while focusing on the actual interesting parts, the idea behind the proof and the possible intuitions for them. Textbook might include them, but as training and because you need to be more explicit when teaching.

edgyquant 4y ago
>Simply not true. Okay. What is a proof other than a step by step explanation for why something’s true? You’re getting caught up in “program” when it’s objectively the case that all math follows a series a steps. A lot of those steps are “handwavy” I’ll give you that. That’s not relevant to what I said though. >there is nothing interesting about symbol manipulation Cool. You missed my entire point again. Math education is geared towards a certain set of people who pick up on (and gain an interest in) the language of math. Only once you get to higher level math do you even start to get alternative visualizations etc (at which point you’ve weeded out a ton of people who would have benefited from e.g. visualizing numbers as groups of shapes). There are a million ways to teach math and we’re leaving a lot of people behind. That was my point
- constantcrying 4y ago
  >Okay. What is a proof other than a step by step explanation for why something’s true? Cooking instructions are a series of steps as well. Would you also claim cooking, mathematics and programming really are all the same thing?
zozbot234 4y ago
A constructive proof of existence is exactly a program. (It might not always be a program for a Turing machine, because "constructive" and "computable" are not exactly the same - but that's beside the point.) Even a non-constructive proof of existence for x can be significant in a programmatic context; it tells you that you can posit an oracle for x (e.g. asking for it to be input by the user, introducing further assumptions based on some special case, etc.) without thereby crashing the program or causing it to behave incorrectly.
- constantcrying 4y ago
  >but that's beside the point It seems to me that it is an important point though. > Even a non-constructive proof of existence for x can be significant in a programmatic context Which has no relation whatsover to proofs and programms being the same thing.
  - zozbot234 4y ago
    A type-level program is still a program. Non-constructive proofs are addressing the question "will this program crash or go wrong if I extend it to do X, regardless of how I achieve that?", which is exactly the domain of type-level programming.
  - logarhythmic 4y ago
    Programs and proofs are the same thing though according to the Curry Howard Correspondence, if I'm not wrong.
hnews_account_1 4y ago
The first part of your answer is incorrect about programming in a general sense (not the particular software programming most of HN does). I push it so far back as to call it programming in a computer science sense, which is very simply just proof theory encoded into a system. There is a reason Turing is considered one of the greatest minds to ever live. He didn’t just invent a concept. He invented a completely new branch of science. We would’ve gotten there eventually but his idea to solve the Entscheidungsproblem using his machine was such a step ahead of the times that we christened him the father of an entire science.
- defrost 4y ago
  Errr, Alonzo Church solved it first, Turing followed .. and both of their independent methods were heavily based upon similar earlier work by Kurt Gödel, with Church also incorporating ideas from Stephen Kleene. There is no doubt that Turing was bright, very bright indeed, but next you'll be claiming he cracked the Enigma Code or something.

edgyquant 4y ago

>Simply not true. Okay. What is a proof other than a step by step explanation for why something’s true? You’re getting caught up in “program” when it’s objectively the case that all math follows a series a steps. A lot of those steps are “handwavy” I’ll give you that. That’s not relevant to what I said though. >there is nothing interesting about symbol manipulation Cool. You missed my entire point again. Math education is geared towards a certain set of people who pick up on (and gain an interest in) the language of math. Only once you get to higher level math do you even start to get alternative visualizations etc (at which point you’ve weeded out a ton of people who would have benefited from e.g. visualizing numbers as groups of shapes). There are a million ways to teach math and we’re leaving a lot of people behind. That was my point

constantcrying 4y ago
>Okay. What is a proof other than a step by step explanation for why something’s true? Cooking instructions are a series of steps as well. Would you also claim cooking, mathematics and programming really are all the same thing?

zozbot234 4y ago

A constructive proof of existence is exactly a program. (It might not always be a program for a Turing machine, because "constructive" and "computable" are not exactly the same - but that's beside the point.) Even a non-constructive proof of existence for x can be significant in a programmatic context; it tells you that you can posit an oracle for x (e.g. asking for it to be input by the user, introducing further assumptions based on some special case, etc.) without thereby crashing the program or causing it to behave incorrectly.

constantcrying 4y ago
>but that's beside the point It seems to me that it is an important point though. > Even a non-constructive proof of existence for x can be significant in a programmatic context Which has no relation whatsover to proofs and programms being the same thing.
- zozbot234 4y ago
  A type-level program is still a program. Non-constructive proofs are addressing the question "will this program crash or go wrong if I extend it to do X, regardless of how I achieve that?", which is exactly the domain of type-level programming.
- logarhythmic 4y ago
  Programs and proofs are the same thing though according to the Curry Howard Correspondence, if I'm not wrong.

hnews_account_1 4y ago

The first part of your answer is incorrect about programming in a general sense (not the particular software programming most of HN does). I push it so far back as to call it programming in a computer science sense, which is very simply just proof theory encoded into a system. There is a reason Turing is considered one of the greatest minds to ever live. He didn’t just invent a concept. He invented a completely new branch of science. We would’ve gotten there eventually but his idea to solve the Entscheidungsproblem using his machine was such a step ahead of the times that we christened him the father of an entire science.

defrost 4y ago
Errr, Alonzo Church solved it first, Turing followed .. and both of their independent methods were heavily based upon similar earlier work by Kurt Gödel, with Church also incorporating ideas from Stephen Kleene. There is no doubt that Turing was bright, very bright indeed, but next you'll be claiming he cracked the Enigma Code or something.