3 ms·

> 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

> 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.)
  - zmonx 9y ago
    For one particular example where homoiconicity makes reasoning about programs easier, consider an important reasoning method called abstract interpretation: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation Using abstract interpretation, you can derive interesting program properties. The uniformity and simplicity of Prolog code, as well as its built-in language constructs like unification and backtracking, make it especially easy to write abstract interpreters for Prolog. Here is a paper that applies this idea to derive several interesting facts about programs and their meaning: Michael Codish and Harald Søndergaard, Meta-circular Abstract Interpretation in Prolog (2002) https://link.springer.com/chapter/10.1007%2F3-540-36377-7_6 https://link.springer.com/chapter/10.1007%2F3-540-36377-7_6 Abstract interpretation is also applicable to other programming languages. However, it is much easier to apply to homoiconic languages like Prolog.
    - kd0amg 9y ago
      Abstract interpretation is entirely about the semantics of programs and has nothing to do with their surface syntax.
      - zmonx 9y ago
        Yes, indeed! Please note that what makes this reasoning method so easily applicable in this case is uniformity of the abstract syntax, not of the surface syntax, which is also called concrete syntax. Homoiconicity is a relation between the concrete and abstract syntax tree (AST) of programs and the language's built-in data structures.
        catnaroek 9y ago
        No idea about you, but when I reason about programs, I spend very little time manipulating syntax. Most of the time is spent manipulating semantic objects, like predicates on the program state, whose representation is independent from even the abstract syntax of a programming language.
  - 9y ago

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.)
- zmonx 9y ago
  For one particular example where homoiconicity makes reasoning about programs easier, consider an important reasoning method called abstract interpretation: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation Using abstract interpretation, you can derive interesting program properties. The uniformity and simplicity of Prolog code, as well as its built-in language constructs like unification and backtracking, make it especially easy to write abstract interpreters for Prolog. Here is a paper that applies this idea to derive several interesting facts about programs and their meaning: Michael Codish and Harald Søndergaard, Meta-circular Abstract Interpretation in Prolog (2002) https://link.springer.com/chapter/10.1007%2F3-540-36377-7_6 https://link.springer.com/chapter/10.1007%2F3-540-36377-7_6 Abstract interpretation is also applicable to other programming languages. However, it is much easier to apply to homoiconic languages like Prolog.
  - kd0amg 9y ago
    Abstract interpretation is entirely about the semantics of programs and has nothing to do with their surface syntax.
    - zmonx 9y ago
      Yes, indeed! Please note that what makes this reasoning method so easily applicable in this case is uniformity of the abstract syntax, not of the surface syntax, which is also called concrete syntax. Homoiconicity is a relation between the concrete and abstract syntax tree (AST) of programs and the language's built-in data structures.
      - catnaroek 9y ago
        No idea about you, but when I reason about programs, I spend very little time manipulating syntax. Most of the time is spent manipulating semantic objects, like predicates on the program state, whose representation is independent from even the abstract syntax of a programming language.
- 9y ago