7 ms·

Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more expli

Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.

icen 6y ago
If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/
kungato 6y ago
Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
- Gravityloss 6y ago
  Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
- nyanpasu64 6y ago
  Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
  - mcaruso 6y ago
    > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
  - throwawaygh 6y ago
    > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
    - nyanpasu64 6y ago
      It was not strictly a logic class, but more of an overview course of discrete math, logic and proofs, and some statistics. They taught -> I think. I've never heard of "sequent calculus" before, and I don't expect anyone I know to have heard it. Apparently it's not calculus. > They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium. I don't think universities are watered down because they don't teach notation that most people don't know and find obscure. My university is famous for a difficult admissions process, tough courses that most people only learn 2/3 of the material, and grading curves calibrated so getting 60% on exams is enough for a B or A. ---- https://en.wikipedia.org/wiki/Sequent_calculus https://en.wikipedia.org/wiki/Sequent_calculus Wikipedia says "Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments." I didn't learn "every statement is conditional" logic involving turnstiles, I learned something where the assumptions were given in the problem, and each line was proven based on the previous lines, which boiled down to the initial givens.
mehrdadn 6y ago
Just in case you're wondering if it's just you: no it's not. PL theory seems almost deliberately designed to make even the most mundane things insanely complicated and difficult to formulate or parse. I'm convinced much of the complexity is absolutely unwarranted and only serves to gate the field to newcomers. It makes things so much more painful than they need to be and turns what could be otherwise a potentially interesting topic into something that's more dry than cardboard.
- throwawaygh 6y ago
  Most of the notation was invented either before or at the dawn of the computer age. It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.
  - mehrdadn 6y ago
    > Most of the notation was invented either before or at the dawn of the computer age. I mean, what's why I said almost? > It's also not particularly difficult to pick up. Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
    - throwawaygh 6y ago
      Our highschoolers pick it up just fine, and are building complicated proofs within 3 lessons. That's not intended as any sort of attack, but it does make it hard for me to believe that the notation is particularly difficult to learn. Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.

icen 6y ago

If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/

kungato 6y ago

Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums

Gravityloss 6y ago
Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
nyanpasu64 6y ago
Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
- mcaruso 6y ago
  > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
- throwawaygh 6y ago
  > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
  - nyanpasu64 6y ago
    It was not strictly a logic class, but more of an overview course of discrete math, logic and proofs, and some statistics. They taught -> I think. I've never heard of "sequent calculus" before, and I don't expect anyone I know to have heard it. Apparently it's not calculus. > They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium. I don't think universities are watered down because they don't teach notation that most people don't know and find obscure. My university is famous for a difficult admissions process, tough courses that most people only learn 2/3 of the material, and grading curves calibrated so getting 60% on exams is enough for a B or A. ---- https://en.wikipedia.org/wiki/Sequent_calculus https://en.wikipedia.org/wiki/Sequent_calculus Wikipedia says "Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments." I didn't learn "every statement is conditional" logic involving turnstiles, I learned something where the assumptions were given in the problem, and each line was proven based on the previous lines, which boiled down to the initial givens.

mehrdadn 6y ago

Just in case you're wondering if it's just you: no it's not. PL theory seems almost deliberately designed to make even the most mundane things insanely complicated and difficult to formulate or parse. I'm convinced much of the complexity is absolutely unwarranted and only serves to gate the field to newcomers. It makes things so much more painful than they need to be and turns what could be otherwise a potentially interesting topic into something that's more dry than cardboard.

throwawaygh 6y ago
Most of the notation was invented either before or at the dawn of the computer age. It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.
- mehrdadn 6y ago
  > Most of the notation was invented either before or at the dawn of the computer age. I mean, what's why I said almost? > It's also not particularly difficult to pick up. Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
  - throwawaygh 6y ago
    Our highschoolers pick it up just fine, and are building complicated proofs within 3 lessons. That's not intended as any sort of attack, but it does make it hard for me to believe that the notation is particularly difficult to learn. Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.