5 ms·

A bit of nitpicking: "the function to compute the truth value of a given proof" should be "the function that returns the truth value of a given statement" (1st

by ASipos 9y ago

A bit of nitpicking: "the function to compute the truth value of a given proof" should be "the function that returns the truth value of a given statement" (1st change because it is confusing to use the word compute in two different ways, 2nd change is simply an error correction) "equivalent in power" should not link to the Church-Turing thesis, as the former is a mathematical statement, proved in any introductory course on computability, and the latter is a philosophical one. w.r.t. the Neil Gaiman quote: https://www.goodreads.com/topic/show/1407558-misattributed-quote https://www.goodreads.com/topic/show/1407558-misattributed-q...

justinpombrio 9y ago
More nitpicking: > You can prove that by writing a simulator for a Turing machine in your language. Since Turing proved his machine can compute any computable function, by induction, that means your language can too. That's not by induction, that's by composition or something. > We almost have the third too. You can create and concatenate strings of arbitrary size, so you can store unbounded memory. That's not true! Eventually you'll run out of memory & disk space. Turing machine tapes are infinite, you can't fit one in this puny universe. EDIT: > Syntactic sugar has a bad rap among the PL intelligentsia. Um, what? I presume the author isn't aware of the large PLT group at Northeastern that continuously writes papers about macros, i.e. user-defined syntactic sugar, and develops Racket, a language built almost entirely out of syntactic sugar. Or maybe they're defining "syntactic sugar" to not include macros: if so, they should be more clear about that. Also, I'm doing a PhD focusing on syntactic sugar, so I probably have authority to say: syntactic sugar has a very good rap among the PL intelligentsia. Languages with a needlessly complicated semantics have a bad rap, but that's different from having a large grammar. PL researchers are a lot more concerned about semantics than syntax.
- munificent 9y ago
  > That's not by induction, that's by composition or something. Good point. I'll fix that. > That's not true! Eventually you'll run out of memory & disk space. Turing machine tapes are infinite, you can't fit one in this puny universe. Sure, but in practice, most people loosen that requirement. Otherwise, no implemented language is Turing-complete. > Um, what? I presume the author isn't aware of the large PLT group at Northeastern that continuously writes papers about macros, i.e. user-defined syntactic sugar, and develops Racket, a language built almost entirely out of syntactic sugar. The mini-essay is about what syntactic sugar the language designer chooses to add to the language. Language features that let users extend the syntax are outside of the scope of that. I do note: > Lispers famously claim their language “has no syntax”, while Smalltalkers proudly show that you can fit the entire grammar on an index card. This tribe has the philosophy that the language doesn’t need syntactic sugar. Instead, the minimal syntax and semantics it provides are powerful enough to let library code be as expressive as if it were part of the language itself.
  - justinpombrio 9y ago
    > The mini-essay is about what syntactic sugar the language designer chooses to add to the language. Language features that let users extend the syntax are outside of the scope of that. What counts as part of the language? If you've coded in a lisp, you've used `and`, `or`, `cond`, `let*`, `letrec`, etc. All of those are defined by macros, but I don't think it's realistic to exclude them from being considered part of the language.
    - kazinator 9y ago
      > What counts as part of the language? Very simple: the arbitrary set of requirements documented in the reference manual for the language and (consequently) provided in the implementation.
      - deleted 9y ago
        [deleted]
  - sigjuice 9y ago
    Common Lisp has a whole bunch of syntax and syntactic sugar. e.g. ' (quote), #', &rest, &key, &optional and more.
  - dom0 9y ago
    > Sure, but in practice, most people loosen that requirement. Otherwise, no implemented language is Turing-complete. The common hand-wave for this is to assume that (1) the machine has big enough storage for the problem, otherwise you could not have the problem in the first place and (2) the algorithm can have an arbitrary time/space trade-off, so if it needed more memory than the physical bound, you could just have it run longer. Note that (1) is a non-sequitur, since the input tape is usually not included in the machine memory in the first place.
- deleted 9y ago
  [deleted]
- DonaldPShimoda 9y ago
  I just wanna add that there is also a dedicated group at Utah working on hygiene and macros for Racket, headed by Matthew Flatt (who's somewhat relevant within the scope of Racket). (Not contradicting you; just wanna throw my school in where I can!)
  - agumonkey 9y ago
    The colored sets ?
    - DonaldPShimoda 9y ago
      I think you mean Flatt's "Binding as Sets of Scopes" [1]. Yeah, that's definitely something he's working on. There are a couple PhD candidates in his group who are also working on macros and hygiene, but I don't follow their research directly (we're just often in the same room so I hear about it). [1] http://www.cs.utah.edu/plt/publications/popl16-f.pdf http://www.cs.utah.edu/plt/publications/popl16-f.pdf
      - agumonkey 9y ago
        Cool, from what I recall Flatt said there were issues in his process so I'm curious about what's new.
        DonaldPShimoda 9y ago
        Ah, I wish I could tell you! He's recently taken on some more teaching duties, so I dunno to what extent that is impacting his research abilities. (Hopefully not too much!)
- agumonkey 9y ago
  May I ask your team website if there's one ? I'm curious about your research
munificent 9y ago
Thanks for this! When I get home this evening, I'll tweak this. You're right on all accounts. Except for the Neil Gaiman quote. I like Gaiman's wording better than Chesterton's and I think it's different enough that it makes sense to attribute it to him. Also, man, what was up that Petêr guy? Who peed in his Cheerios?
- sn9 9y ago
  > "It turns out that the answer to both is “no” and, in astonishingly, the two questions are deeply intertwined." Did you forget a word here?
  - munificent 9y ago
    Yes, yes I did. Would you believe I did three drafts of this? I'll fix it tonight. Thanks!
    - sn9 9y ago
      Haha I wouldn't worry about it. I've seen more typos in professionally edited articles on major online newspapers.
  - yorwba 9y ago
    Related to that, the two questions are > “Can all true statements be proven?”, “Are there functions that we can define but not compute?” And the answers are "no" and "yes", so to fit with "both answers are 'no'", the second question should be "Can we compute all functions we can define?".
    - munificent 9y ago
      Oh, God, you're right. Thank you! You wouldn't know I actually edited this chapter twice.

by ASipos 9y ago

justinpombrio 9y ago

More nitpicking: > You can prove that by writing a simulator for a Turing machine in your language. Since Turing proved his machine can compute any computable function, by induction, that means your language can too. That's not by induction, that's by composition or something. > We almost have the third too. You can create and concatenate strings of arbitrary size, so you can store unbounded memory. That's not true! Eventually you'll run out of memory & disk space. Turing machine tapes are infinite, you can't fit one in this puny universe. EDIT: > Syntactic sugar has a bad rap among the PL intelligentsia. Um, what? I presume the author isn't aware of the large PLT group at Northeastern that continuously writes papers about macros, i.e. user-defined syntactic sugar, and develops Racket, a language built almost entirely out of syntactic sugar. Or maybe they're defining "syntactic sugar" to not include macros: if so, they should be more clear about that. Also, I'm doing a PhD focusing on syntactic sugar, so I probably have authority to say: syntactic sugar has a very good rap among the PL intelligentsia. Languages with a needlessly complicated semantics have a bad rap, but that's different from having a large grammar. PL researchers are a lot more concerned about semantics than syntax.

munificent 9y ago
> That's not by induction, that's by composition or something. Good point. I'll fix that. > That's not true! Eventually you'll run out of memory & disk space. Turing machine tapes are infinite, you can't fit one in this puny universe. Sure, but in practice, most people loosen that requirement. Otherwise, no implemented language is Turing-complete. > Um, what? I presume the author isn't aware of the large PLT group at Northeastern that continuously writes papers about macros, i.e. user-defined syntactic sugar, and develops Racket, a language built almost entirely out of syntactic sugar. The mini-essay is about what syntactic sugar the language designer chooses to add to the language. Language features that let users extend the syntax are outside of the scope of that. I do note: > Lispers famously claim their language “has no syntax”, while Smalltalkers proudly show that you can fit the entire grammar on an index card. This tribe has the philosophy that the language doesn’t need syntactic sugar. Instead, the minimal syntax and semantics it provides are powerful enough to let library code be as expressive as if it were part of the language itself.
- justinpombrio 9y ago
  > The mini-essay is about what syntactic sugar the language designer chooses to add to the language. Language features that let users extend the syntax are outside of the scope of that. What counts as part of the language? If you've coded in a lisp, you've used `and`, `or`, `cond`, `let*`, `letrec`, etc. All of those are defined by macros, but I don't think it's realistic to exclude them from being considered part of the language.
  - kazinator 9y ago
    > What counts as part of the language? Very simple: the arbitrary set of requirements documented in the reference manual for the language and (consequently) provided in the implementation.
    - deleted 9y ago
      [deleted]
- sigjuice 9y ago
  Common Lisp has a whole bunch of syntax and syntactic sugar. e.g. ' (quote), #', &rest, &key, &optional and more.
- dom0 9y ago
  > Sure, but in practice, most people loosen that requirement. Otherwise, no implemented language is Turing-complete. The common hand-wave for this is to assume that (1) the machine has big enough storage for the problem, otherwise you could not have the problem in the first place and (2) the algorithm can have an arbitrary time/space trade-off, so if it needed more memory than the physical bound, you could just have it run longer. Note that (1) is a non-sequitur, since the input tape is usually not included in the machine memory in the first place.
deleted 9y ago
[deleted]
DonaldPShimoda 9y ago
I just wanna add that there is also a dedicated group at Utah working on hygiene and macros for Racket, headed by Matthew Flatt (who's somewhat relevant within the scope of Racket). (Not contradicting you; just wanna throw my school in where I can!)
- agumonkey 9y ago
  The colored sets ?
  - DonaldPShimoda 9y ago
    I think you mean Flatt's "Binding as Sets of Scopes" [1]. Yeah, that's definitely something he's working on. There are a couple PhD candidates in his group who are also working on macros and hygiene, but I don't follow their research directly (we're just often in the same room so I hear about it). [1] http://www.cs.utah.edu/plt/publications/popl16-f.pdf http://www.cs.utah.edu/plt/publications/popl16-f.pdf
    - agumonkey 9y ago
      Cool, from what I recall Flatt said there were issues in his process so I'm curious about what's new.
      - DonaldPShimoda 9y ago
        Ah, I wish I could tell you! He's recently taken on some more teaching duties, so I dunno to what extent that is impacting his research abilities. (Hopefully not too much!)
agumonkey 9y ago
May I ask your team website if there's one ? I'm curious about your research

munificent 9y ago

Thanks for this! When I get home this evening, I'll tweak this. You're right on all accounts. Except for the Neil Gaiman quote. I like Gaiman's wording better than Chesterton's and I think it's different enough that it makes sense to attribute it to him. Also, man, what was up that Petêr guy? Who peed in his Cheerios?

sn9 9y ago
> "It turns out that the answer to both is “no” and, in astonishingly, the two questions are deeply intertwined." Did you forget a word here?
- munificent 9y ago
  Yes, yes I did. Would you believe I did three drafts of this? I'll fix it tonight. Thanks!
  - sn9 9y ago
    Haha I wouldn't worry about it. I've seen more typos in professionally edited articles on major online newspapers.
- yorwba 9y ago
  Related to that, the two questions are > “Can all true statements be proven?”, “Are there functions that we can define but not compute?” And the answers are "no" and "yes", so to fit with "both answers are 'no'", the second question should be "Can we compute all functions we can define?".
  - munificent 9y ago
    Oh, God, you're right. Thank you! You wouldn't know I actually edited this chapter twice.