3 ms·

> very easy to reason [sic] about by built-in mechanisms in that language. Languages allow you to express your reasoning, but they don't do the reasoning by th

> very easy to reason [sic] about by built-in mechanisms in that language. Languages allow you to express your reasoning, but they don't do the reasoning by themselves. Also, there is no conclusive evidence that homoiconic languages have simpler semantics, especially of the denotational kind.

taeric 9y ago
I think the meaning is that fewer things are implemented by bringing in outside capabilities. In lisp, everything's can be expressed in terms of other lisp code. Typically directly so. In other languages that are not as macro friendly, most keywords get the explanation of "this is how the computer will act" and then explanations of new behaviors.
- catnaroek 9y ago
  > In lisp, everything's can be expressed in terms of other lisp code. Um, and how exactly are primitive forms defined? > most keywords get the explanation of "this is how the computer will act" and then explanations of new behaviors. Have you heard of Hoare logic? The meaning of ordinary ALGOL-style imperative programs can be given in terms of relating preconditions to postconditions. Suppose that you have the Hoare triples: {P} foo {Q} {Q} bar {R} Then you can derive the Hoare triple: {P} foo; bar {R} Note that `Q` is not mentioned at all. Hence, any implementation is free to translate the program foo; bar into something that doesn't have `Q` as an intermediate state.
  - taeric 9y ago
    You seem to be arguing past me. If you are just upset that I said everything instead of most things, yeah, obviously some things are defined elsewhere. To that end, how things are actually implemented takes a trip to assembly. (I mainly blame that I'm writing in my phone. Often while in the bus.) My point was that you don't typically see c constructs explained in terms of other c constructs. This is quite common in lisp. To see lisp constructs explained in terms of other lisp constructs. In large because there are few constructs. You showing me that you can explain using other logic is kind of my point. It is awesome that you can do this. I recommend the skill. It is still not showing c or Java or Haskell or whatever in terms of themselves. Note that I think you actually can do this, in large. It is not typically done, though.
    - catnaroek 9y ago
      > To that end, how things are actually implemented takes a trip to assembly. Don't confuse “defined” with “implemented”. This is the entire point to having an axiomatic semantics! > My point was that you don't typically see c constructs explained in terms of other c constructs. Languages can't be entirely defined in terms of themselves. At some point you need to drop down to something else. If most of Lisp is defined in terms of other Lisp constructs, that is perfectly fine, but, for my purposes, i.e., proving things about programs, there are two mutually exclusive possibilities: (0) The semantics of Lisp is the semantics of its primitive forms, and derived forms are just Lisp's standard library. (1) So-called “derived” forms have an abstract semantics of their own right, and their implementation in terms of so-called “primitive” forms is, well, an implementation detail. So, my answer to “most of Lisp is defined in terms of Lisp itself” is “that's cute, but how mathematically elegant is the part of Lisp that is not defined in terms of itself?”
      - taeric 9y ago
        I said explained. Not defined. Not implemented. Definitely not proved. Just explained. There is typically exposition, as well. So, by all means, keep arguing points I'm not making. I was offering what I suspect the parent post meant by it being easier to reason using the mechanics of the language. Nothing more.
        catnaroek 9y ago
        > I was offering what I suspect the parent post meant by it being easier to reason using the mechanics of the language. And it still doesn't make sense. “Reasoning about programs” is making inferences about their meaning, i.e., deriving judgments from prior judgments. How exactly do homoiconic languages make it any easier to make inferences about the meaning of programs, given that homoiconicity is largely a property of how concrete and abstract syntaxes are related to each other? (Not that homoiconicity makes things more difficult either. It is just completely unrelated to reasoning about programs.)
        9y ago

taeric 9y ago

I think the meaning is that fewer things are implemented by bringing in outside capabilities. In lisp, everything's can be expressed in terms of other lisp code. Typically directly so. In other languages that are not as macro friendly, most keywords get the explanation of "this is how the computer will act" and then explanations of new behaviors.

catnaroek 9y ago
> In lisp, everything's can be expressed in terms of other lisp code. Um, and how exactly are primitive forms defined? > most keywords get the explanation of "this is how the computer will act" and then explanations of new behaviors. Have you heard of Hoare logic? The meaning of ordinary ALGOL-style imperative programs can be given in terms of relating preconditions to postconditions. Suppose that you have the Hoare triples: {P} foo {Q} {Q} bar {R} Then you can derive the Hoare triple: {P} foo; bar {R} Note that `Q` is not mentioned at all. Hence, any implementation is free to translate the program foo; bar into something that doesn't have `Q` as an intermediate state.
- taeric 9y ago
  You seem to be arguing past me. If you are just upset that I said everything instead of most things, yeah, obviously some things are defined elsewhere. To that end, how things are actually implemented takes a trip to assembly. (I mainly blame that I'm writing in my phone. Often while in the bus.) My point was that you don't typically see c constructs explained in terms of other c constructs. This is quite common in lisp. To see lisp constructs explained in terms of other lisp constructs. In large because there are few constructs. You showing me that you can explain using other logic is kind of my point. It is awesome that you can do this. I recommend the skill. It is still not showing c or Java or Haskell or whatever in terms of themselves. Note that I think you actually can do this, in large. It is not typically done, though.
  - catnaroek 9y ago
    > To that end, how things are actually implemented takes a trip to assembly. Don't confuse “defined” with “implemented”. This is the entire point to having an axiomatic semantics! > My point was that you don't typically see c constructs explained in terms of other c constructs. Languages can't be entirely defined in terms of themselves. At some point you need to drop down to something else. If most of Lisp is defined in terms of other Lisp constructs, that is perfectly fine, but, for my purposes, i.e., proving things about programs, there are two mutually exclusive possibilities: (0) The semantics of Lisp is the semantics of its primitive forms, and derived forms are just Lisp's standard library. (1) So-called “derived” forms have an abstract semantics of their own right, and their implementation in terms of so-called “primitive” forms is, well, an implementation detail. So, my answer to “most of Lisp is defined in terms of Lisp itself” is “that's cute, but how mathematically elegant is the part of Lisp that is not defined in terms of itself?”
    - taeric 9y ago
      I said explained. Not defined. Not implemented. Definitely not proved. Just explained. There is typically exposition, as well. So, by all means, keep arguing points I'm not making. I was offering what I suspect the parent post meant by it being easier to reason using the mechanics of the language. Nothing more.
      - catnaroek 9y ago
        > I was offering what I suspect the parent post meant by it being easier to reason using the mechanics of the language. And it still doesn't make sense. “Reasoning about programs” is making inferences about their meaning, i.e., deriving judgments from prior judgments. How exactly do homoiconic languages make it any easier to make inferences about the meaning of programs, given that homoiconicity is largely a property of how concrete and abstract syntaxes are related to each other? (Not that homoiconicity makes things more difficult either. It is just completely unrelated to reasoning about programs.)
        9y ago