5 ms·

Maybe if you view "programming" as one homogenous block of understanding, but there is a difference between doing basic low-level programming and effectively wr

Maybe if you view "programming" as one homogenous block of understanding, but there is a difference between doing basic low-level programming and effectively writing abstract code in Haskell. I can only speak for myself but layers of abstraction make things exponentially harder for me to follow. Compact mathematical notation on top of that feels a bit exhausting. It can probably be called accessible for people already interested or talented in maths, but there's a reason most people don't just casually learn astrophysics for fun even though some introductory material might be considered accessible - not everyone can do it without unreasonable amounts of effort.

the_af 3y ago
> Maybe if you view "programming" as one homogenous block of understanding Oh, I'm not saying it's the same as programming in your favorite language. I'm saying if you have the mental machinery to understand a new language, you also have it to learn lambda calculus. Trust me, it's not that hard. It just looks extraneous out of context because you are not familiar with it. > It can probably be called accessible for people already interested or talented in maths I'm not particularly good at maths and I found introductory-level lambda calculus not very difficult. The notation is different from, say, a C program. You just learn this notation, which your professor will explain. Nothing too terrible. > layers of abstraction I'm confused. Which layers of abstraction? I mean, it's an abstraction just like C or Python or "1 + 1" are abstractions. There are rules and you learn how to apply them.
- _a_a_a_ 3y ago
  It's about the entire set of formalisms given in the pdf, not just lambda calculus. The argument here about LC was because I had just given a snippet of it, but it's not the whole paper. Now, the next bit – so I've spent my 15 minutes reading up on each of these formalisms (lambda calculus, intuitionistic logic, Hoare notation, whatever else). So now I can read the paper and I do, and now I have absolutely no way of making use of anything I've learnt. I spent personally a lot of time on the computer science side of things, and I have got frankly just about nothing out of it. So frankly again, there's no point learning it (from a utilitarian perspective). When I was a kid I picked up a book on Fortran 4 and tried to learn it from the book, without a computer. That's pretty much the situation here – a passive notation that, had I managed to internalise it, would have been completely useless because I had no computer to run it on. And I'm tired of this discussion of people saying it's easy and it's useful, because it's not easy, and it's not useful without a whole lot more studying an application to bridge the abstraction of the formalism to the actual programming environment where I can use it. Please just stop repeating stuff.
  - vilhelm_s 3y ago
    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.
emporas 3y ago
Certain proofs about a program, implemented using types, are useful in high level programming, as well as low level programming. See Rust in the linux kernel [1], and Rust on Android[2]. One way to think about it, is that proofs about a program are a continuum, rather than one or the other. Sure, going all the way, disallowing mutability and requiring types for everything, might make the system more provable, but slower as well. There are some different ways to look at a program: Corporate developer: "Programs are to be run, and occasionally read or proved correctly" Donald Knuth: "Programs are to be read, and occasionally run" Type Theorist: "Programs are to be compiled, and occasionally run or read" https://thenewstack.io/rust-in-the-linux-kernel/ https://thenewstack.io/rust-in-the-linux-kernel/ https://security.googleblog.com/2023/10/bare-metal-rust-in-android.html https://security.googleblog.com/2023/10/bare-metal-rust-in-a...

the_af 3y ago

> Maybe if you view "programming" as one homogenous block of understanding Oh, I'm not saying it's the same as programming in your favorite language. I'm saying if you have the mental machinery to understand a new language, you also have it to learn lambda calculus. Trust me, it's not that hard. It just looks extraneous out of context because you are not familiar with it. > It can probably be called accessible for people already interested or talented in maths I'm not particularly good at maths and I found introductory-level lambda calculus not very difficult. The notation is different from, say, a C program. You just learn this notation, which your professor will explain. Nothing too terrible. > layers of abstraction I'm confused. Which layers of abstraction? I mean, it's an abstraction just like C or Python or "1 + 1" are abstractions. There are rules and you learn how to apply them.

_a_a_a_ 3y ago
It's about the entire set of formalisms given in the pdf, not just lambda calculus. The argument here about LC was because I had just given a snippet of it, but it's not the whole paper. Now, the next bit – so I've spent my 15 minutes reading up on each of these formalisms (lambda calculus, intuitionistic logic, Hoare notation, whatever else). So now I can read the paper and I do, and now I have absolutely no way of making use of anything I've learnt. I spent personally a lot of time on the computer science side of things, and I have got frankly just about nothing out of it. So frankly again, there's no point learning it (from a utilitarian perspective). When I was a kid I picked up a book on Fortran 4 and tried to learn it from the book, without a computer. That's pretty much the situation here – a passive notation that, had I managed to internalise it, would have been completely useless because I had no computer to run it on. And I'm tired of this discussion of people saying it's easy and it's useful, because it's not easy, and it's not useful without a whole lot more studying an application to bridge the abstraction of the formalism to the actual programming environment where I can use it. Please just stop repeating stuff.
- vilhelm_s 3y ago
  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.

emporas 3y ago

Certain proofs about a program, implemented using types, are useful in high level programming, as well as low level programming. See Rust in the linux kernel [1], and Rust on Android[2]. One way to think about it, is that proofs about a program are a continuum, rather than one or the other. Sure, going all the way, disallowing mutability and requiring types for everything, might make the system more provable, but slower as well. There are some different ways to look at a program: Corporate developer: "Programs are to be run, and occasionally read or proved correctly" Donald Knuth: "Programs are to be read, and occasionally run" Type Theorist: "Programs are to be compiled, and occasionally run or read" https://thenewstack.io/rust-in-the-linux-kernel/ https://thenewstack.io/rust-in-the-linux-kernel/ https://security.googleblog.com/2023/10/bare-metal-rust-in-android.html https://security.googleblog.com/2023/10/bare-metal-rust-in-a...