Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
It's not supposed to be insulting. I think the notation is more than offputting, and describing it as a barrier to entry is appropriate.
Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
In my experience, any sufficiently deep study of any subject requires introduction of at least some degree of specialized terminology ("jargon") to be able to express things precisely and concisely. Sure, you can try to avoid this and use just "generic" language, but you almost always have to sacrifice one or both of these, at least partially. That can very well be worth it in certain cases (e.g. in an introductory text). But the site being discussed here is a list of specific (counter)examples. It would seem counterproductive to me to "dumb it down" given that it's primary purpose seems to be to discuss very specific situations; indeed, one common feature among many of these examples are subtle differences in what things mean in different parts of a language specification -- i.e., one of the reasons why domain experts invariably start using jargon.
That said, of course jargon often is als abused, or used in cases it doesn't have to be, etc. -- that's s bad! And many papers and books suffer from this and would be improved by using less jargon.
But in general I find this negative stance against formal notation, and the expectation that one should be able to dive into subtle and advanced examples without a need of at least some
"studying" (not at all necessarily at a university!) quite odd, and unrealistic.
I don't get it, do you feel like you need a class in a university to learn programming? Source code is nothing but formal notation. The fact that it kind of looks like English text if you squint makes no difference, as far as I'm concerned. There's only a handful of symbols you have to learn to read type theory stuff.
I believe you that it wasn’t intended to be insulting.
But let’s think about it.
I feel pretty confident that most people on this website are capable of learning the core 2400 Chinese characters in a year if they spent a few hours a day and that’s literally a foreign notation. A lot of people learn new languages all the time.
Kids who don’t want to learn calculus, learn calculus every day. The notation isn’t just awkward, the concepts are too. Yet they learn it.
What we’re talking about is a small notation. It’s a handful of symbols. They work predictably and consistently and the people learning it are usually familiar with the subject on some level.
It’s off-putting because it appears foreign, but the concepts and actual mechanics are already familiar with most of these readers. They just need a Rosetta Stone to help get past the initial awkwardness.
When you look at it from that perspective, it is kind of insulting use a hyperbolic word like insurmountable to a group of programmers.
Many chose not to learn it because they don’t want to be bother or don’t see the value investing their time.
Throwing words like insurmountable around seems like it breeds learned helplessness.
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation.
Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book.
Inference rules just transform the traditional format of
(A && B) -> C
into
A B
---
C
This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
It's interesting how calling it insurmountable both panders to and insults the people you're talking about.
Maybe a better way to describe the notation is "off-putting"?
It's not supposed to be insulting. I think the notation is more than offputting, and describing it as a barrier to entry is appropriate.
Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
In my experience, any sufficiently deep study of any subject requires introduction of at least some degree of specialized terminology ("jargon") to be able to express things precisely and concisely. Sure, you can try to avoid this and use just "generic" language, but you almost always have to sacrifice one or both of these, at least partially. That can very well be worth it in certain cases (e.g. in an introductory text). But the site being discussed here is a list of specific (counter)examples. It would seem counterproductive to me to "dumb it down" given that it's primary purpose seems to be to discuss very specific situations; indeed, one common feature among many of these examples are subtle differences in what things mean in different parts of a language specification -- i.e., one of the reasons why domain experts invariably start using jargon.
That said, of course jargon often is als abused, or used in cases it doesn't have to be, etc. -- that's s bad! And many papers and books suffer from this and would be improved by using less jargon.
But in general I find this negative stance against formal notation, and the expectation that one should be able to dive into subtle and advanced examples without a need of at least some "studying" (not at all necessarily at a university!) quite odd, and unrealistic.
19 replies →
I don't get it, do you feel like you need a class in a university to learn programming? Source code is nothing but formal notation. The fact that it kind of looks like English text if you squint makes no difference, as far as I'm concerned. There's only a handful of symbols you have to learn to read type theory stuff.
I believe you that it wasn’t intended to be insulting.
But let’s think about it.
I feel pretty confident that most people on this website are capable of learning the core 2400 Chinese characters in a year if they spent a few hours a day and that’s literally a foreign notation. A lot of people learn new languages all the time.
Kids who don’t want to learn calculus, learn calculus every day. The notation isn’t just awkward, the concepts are too. Yet they learn it.
What we’re talking about is a small notation. It’s a handful of symbols. They work predictably and consistently and the people learning it are usually familiar with the subject on some level.
It’s off-putting because it appears foreign, but the concepts and actual mechanics are already familiar with most of these readers. They just need a Rosetta Stone to help get past the initial awkwardness.
When you look at it from that perspective, it is kind of insulting use a hyperbolic word like insurmountable to a group of programmers.
Many chose not to learn it because they don’t want to be bother or don’t see the value investing their time.
Throwing words like insurmountable around seems like it breeds learned helplessness.
4 replies →
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation.
At least BNF grammars are legible
Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book.
Inference rules just transform the traditional format of
into
This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
It seems absurd to care about 'page space' when discussing computer science notation...
ah notation is such a subtle and often sad topic
when you click you never give a damn about notation but before you do it's such a drag
it's like monads