5 ms·

Ok, but now you are making a completely different claim! You started out saying, "oh, these lecture requires some advanced math background to understand", and

Ok, but now you are making a completely different claim! You started out saying, "oh, these lecture requires some advanced math background to understand", and quoted the curry function. And then a lot of people explained that no, there is no advanced math, this is just a function written in a programming language. And now it seems you agree, if you spend only 15 minutes you can understand the lecture notes. That's all I, and others, wanted to say. Separately, it's the case that understanding this will not be very useful in a day-to-day programming job. That's just because it's not all that useful! (See other discussion on this this same HN page.) I think it is very cool and philosophically interesting in itself, and it offers an interesting point of view if you are designing new programming language type systems, but it doesn't have very much "utilitarian" use.

_a_a_a_ 3y ago
> And now it seems you agree, if you spend only 15 minutes you can understand the lecture notes that was sarcasm. > I think it is very cool and philosophically interesting in itself, and it offers an interesting point of view if you are designing new programming language type systems, but it doesn't have very much "utilitarian" use. It has phenomenal use is my point (eg. formal verification, an interest of mine), but only at a vastly higher level than "I've been to the lectures". What I keep saying is, most people aren't interested in the abstract, and neither am I. Give me a practical application and suddenly I'll 'get it'. Without that application it's valueless because I have no reason to engage with it, and actually cannot. Put another way: its application and its understanding are interlinked. You can separate them; I and others can't. I know this stuff is useful and I literally spent years trying to understand it. For someone like me it just isn't easy, and you keep persistently not understanding that.
- hnfong 3y ago
  I'm going to be cynical and make the following observation: Given that there's this correspondence between Math and Programming Languages, what it says is just that if you understand types in programming language, there's no point in understanding the notations in math. And this is especially true if you take a cynical attitude towards theorem provers in the sense that real proofs are in the minds of the thinker, not in the formalism. The fact that the Curry-Howard correspondence is was proposed in the 1930s suggests that it was a relatively "primitive" analogy that might be restated in some obvious way in today's language of computation. Maybe... "you can write programs to be automated theorem provers for formal systems"? I wonder what CS people would have to say about the efforts "to prove a program correct". If a program is equivalent to a proof, "proving a program correct" seems to be "proving a proof correct". I don't really know what I'm talking about though.
  - _a_a_a_ 3y ago
    A program is not a proof.
  - sordina 3y ago
    You've got the right idea. A program is a proof for the proposition made by its type. Only for the right languages though, and not in the naive sense of `assert(1+1 == 2)` proves the assertion.
    - _a_a_a_ 3y ago
      OK, not what I expected. Surely a spec is a spec, the program fulfils the spec hopefully, and the proof is that the program implements the spec. How do you see it? thanks
      - sordina 3y ago
        Curry Howard shows that for a logical proposition (A) with corresponding constructive proof (B), there will be a type (A') with program (B'). It's not about proving desired properties of programs. However, you can use the CH principles to do this too, as long as you can encode the proposition about a program in its type. This will not often look like the dataflow type of the naive program though. Look at software foundations for real detail, I'm not expert at this stuff, just aware of the basics.

_a_a_a_ 3y ago

> And now it seems you agree, if you spend only 15 minutes you can understand the lecture notes that was sarcasm. > I think it is very cool and philosophically interesting in itself, and it offers an interesting point of view if you are designing new programming language type systems, but it doesn't have very much "utilitarian" use. It has phenomenal use is my point (eg. formal verification, an interest of mine), but only at a vastly higher level than "I've been to the lectures". What I keep saying is, most people aren't interested in the abstract, and neither am I. Give me a practical application and suddenly I'll 'get it'. Without that application it's valueless because I have no reason to engage with it, and actually cannot. Put another way: its application and its understanding are interlinked. You can separate them; I and others can't. I know this stuff is useful and I literally spent years trying to understand it. For someone like me it just isn't easy, and you keep persistently not understanding that.

hnfong 3y ago
I'm going to be cynical and make the following observation: Given that there's this correspondence between Math and Programming Languages, what it says is just that if you understand types in programming language, there's no point in understanding the notations in math. And this is especially true if you take a cynical attitude towards theorem provers in the sense that real proofs are in the minds of the thinker, not in the formalism. The fact that the Curry-Howard correspondence is was proposed in the 1930s suggests that it was a relatively "primitive" analogy that might be restated in some obvious way in today's language of computation. Maybe... "you can write programs to be automated theorem provers for formal systems"? I wonder what CS people would have to say about the efforts "to prove a program correct". If a program is equivalent to a proof, "proving a program correct" seems to be "proving a proof correct". I don't really know what I'm talking about though.
- _a_a_a_ 3y ago
  A program is not a proof.
- sordina 3y ago
  You've got the right idea. A program is a proof for the proposition made by its type. Only for the right languages though, and not in the naive sense of `assert(1+1 == 2)` proves the assertion.
  - _a_a_a_ 3y ago
    OK, not what I expected. Surely a spec is a spec, the program fulfils the spec hopefully, and the proof is that the program implements the spec. How do you see it? thanks
    - sordina 3y ago
      Curry Howard shows that for a logical proposition (A) with corresponding constructive proof (B), there will be a type (A') with program (B'). It's not about proving desired properties of programs. However, you can use the CH principles to do this too, as long as you can encode the proposition about a program in its type. This will not often look like the dataflow type of the naive program though. Look at software foundations for real detail, I'm not expert at this stuff, just aware of the basics.