6 ms·

Since when is it a requirement that a programming language be efficient? My larger point is that he seems to be using "programming language" as a shorthand for

by cwyers 8y ago

Since when is it a requirement that a programming language be efficient? My larger point is that he seems to be using "programming language" as a shorthand for an imperative, typed programming language. A lot of what he says doesn't seem to apply very well to SQL or Prolog or Lisp, for instance. (I say this having only skimmed the slides, I don't have two hours for this right now.) I won't say that it's a straw man, because there are plenty of programming languages that fit the way he's using the term and some of them are incredibly popular, but it seems to be a definition that leaves out a lot of programming languages.

pron 8y ago
> Since when is it a requirement that a programming language be efficient? It is (generally) a requirement that if you're writing a linear time algorithm, then the compiled/interpreted language will be executed in linear time. This is not the case for TLA+. You can describe linear time algorithms in a way that can only be compiled into, say, an exponential-time program, and possibly even not at all (i.e., extracting an implementation is undecidable). I wrote about this at some length here: https://pron.github.io/posts/tlaplus_part3 https://pron.github.io/posts/tlaplus_part3 > My larger point is that he seems to be using "programming language" as a shorthand for an imperative, typed programming language He means a language with the property I mentioned above. It is somewhat true that Prolog has a tiny portion of the expressive power that comes from a truly nondeterministic language such as TLA+, but it still falls under "programming language." If you want to get technical, a language such as Prolog can let you program with some limited use of quantifiers. In TLA+, you can specify using unlimited use of quantifiers ranging over infinite and even uncountable domains. In TLA+ you can describe the property "decides halting in linear time," and then show that a specific implementation can do so in some special cases for example. No programming language can do that (i.e. describe non-computable "algorithms") but it is essential for specification languages.
- Jweb_Guru 8y ago
  > No programming language can do that (i.e. describe non-computable "algorithms") Coq certainly can describe properties like this; they're just uninhabited types (all the necessary concepts needed to define "decides halting in linear time" can be defined over an inductive definition of the step function for the programming language of the halting decider; or if what you in fact meant was "a type that represents programs that halt in linear time", it's even easier and requires the same concepts, but a less powerful programming language). There is no specification sublanguage required. I find your distinction to be pretty iffy. Of course, Coq is not a very traditional programming language, but it is a programming language nonetheless. (I note that you claim that Coq separates types and terms into two different semantic and syntactic categories, which isn't really true. The set model, which is the standard model that justifies the consistency of the calculus of inductive constructions, makes no such distinction!).
  - pron 8y ago
    Typed programming languages (any typed formal systems, for that matter) are made of two languages, type level and term/object level. While the two are strongly related, they are separate (a term can inhabit a type, but not another term). The level of nondeterminism required for specification exists at the type level and not at the term level, while programming (in the sense I defined above) exists only at the term level. This is what I meant when I said above that a specification language can be embedded into a programming language (this doesn't require types, but can also be done with contracts), but those are still two languages, even if they share syntax. If you like, you can think of TLA+ as being entirely at the type level.
    - Jweb_Guru 8y ago
      My point is that there are models of (essentially) Coq where there is no distinction between types and terms; both are translated into sets, in a fairly straightforward way. Additionally, one of the major points of dependent type theory is that reduction can occur anywhere, including directly within a type; i.e. term and type cannot be defined separately from one another. I'll go further and say that the fact that a term can only inhabit a type is in some sense definitional, since types are also terms; I can quite easily perform reduction and programming in a term that includes quantifiers, which you would say was part of the nondeterministic type level (in other words, terms do inhabit other terms). So it is extremely unclear to me that the distinction you are making is fundamental. (To be clear, I do agree that there is a difference between specifying a type and synthesizing an inhabitant for that type; I just think that the "programming-specification" distinction you are making is somewhat artificial, with dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well).
      - deleted 8y ago
        [deleted]
      - pron 8y ago
        > My point is that there are models of (essentially) Coq where there is no distinction between types and terms I don't think this is true for Coq. Ultimately, Coq relies on a type/inhabitant separation. When you spoke of Coq as a programming language, the terms you can always "run" are only the inhabitants. > So it is extremely unclear to me that the distinction you are making is fundamental. I don't know if it is entirely binary, but it is sufficiently precise for useful terminology. A programming language is a language that can be used for programming, namely it is a language whose every term can be mechanically interpreted in an "efficient manner." > dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well I don't think that any existing dependently typed languages do anything particularly effectively (neither programming nor specification), but that is beside the point :) It is certainly possible to combine a specification language and a programming language, but not without some formal delineation or the experience would be frustrating (i.e., it is possible to interpret some subset of TLA+ terms, but I am not sure it can be syntactically easy to determine which). This is, however, something that TLA+ tries hard to avoid as a design principle, because we do not yet know of any feasible way to scale specification from the "program level" to arbitrary levels of interest. Unlike Coq, TLA+ was designed not as a research tool for logicians, but as an industrial-strength tool for practitioners (I wrote about the design principles behind TLA+ in part 1 of my series: https://pron.github.io/tlaplus https://pron.github.io/tlaplus).

by cwyers 8y ago

pron 8y ago

> Since when is it a requirement that a programming language be efficient? It is (generally) a requirement that if you're writing a linear time algorithm, then the compiled/interpreted language will be executed in linear time. This is not the case for TLA+. You can describe linear time algorithms in a way that can only be compiled into, say, an exponential-time program, and possibly even not at all (i.e., extracting an implementation is undecidable). I wrote about this at some length here: https://pron.github.io/posts/tlaplus_part3 https://pron.github.io/posts/tlaplus_part3 > My larger point is that he seems to be using "programming language" as a shorthand for an imperative, typed programming language He means a language with the property I mentioned above. It is somewhat true that Prolog has a tiny portion of the expressive power that comes from a truly nondeterministic language such as TLA+, but it still falls under "programming language." If you want to get technical, a language such as Prolog can let you program with some limited use of quantifiers. In TLA+, you can specify using unlimited use of quantifiers ranging over infinite and even uncountable domains. In TLA+ you can describe the property "decides halting in linear time," and then show that a specific implementation can do so in some special cases for example. No programming language can do that (i.e. describe non-computable "algorithms") but it is essential for specification languages.

Jweb_Guru 8y ago
> No programming language can do that (i.e. describe non-computable "algorithms") Coq certainly can describe properties like this; they're just uninhabited types (all the necessary concepts needed to define "decides halting in linear time" can be defined over an inductive definition of the step function for the programming language of the halting decider; or if what you in fact meant was "a type that represents programs that halt in linear time", it's even easier and requires the same concepts, but a less powerful programming language). There is no specification sublanguage required. I find your distinction to be pretty iffy. Of course, Coq is not a very traditional programming language, but it is a programming language nonetheless. (I note that you claim that Coq separates types and terms into two different semantic and syntactic categories, which isn't really true. The set model, which is the standard model that justifies the consistency of the calculus of inductive constructions, makes no such distinction!).
- pron 8y ago
  Typed programming languages (any typed formal systems, for that matter) are made of two languages, type level and term/object level. While the two are strongly related, they are separate (a term can inhabit a type, but not another term). The level of nondeterminism required for specification exists at the type level and not at the term level, while programming (in the sense I defined above) exists only at the term level. This is what I meant when I said above that a specification language can be embedded into a programming language (this doesn't require types, but can also be done with contracts), but those are still two languages, even if they share syntax. If you like, you can think of TLA+ as being entirely at the type level.
  - Jweb_Guru 8y ago
    My point is that there are models of (essentially) Coq where there is no distinction between types and terms; both are translated into sets, in a fairly straightforward way. Additionally, one of the major points of dependent type theory is that reduction can occur anywhere, including directly within a type; i.e. term and type cannot be defined separately from one another. I'll go further and say that the fact that a term can only inhabit a type is in some sense definitional, since types are also terms; I can quite easily perform reduction and programming in a term that includes quantifiers, which you would say was part of the nondeterministic type level (in other words, terms do inhabit other terms). So it is extremely unclear to me that the distinction you are making is fundamental. (To be clear, I do agree that there is a difference between specifying a type and synthesizing an inhabitant for that type; I just think that the "programming-specification" distinction you are making is somewhat artificial, with dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well).
    - deleted 8y ago
      [deleted]
    - pron 8y ago
      > My point is that there are models of (essentially) Coq where there is no distinction between types and terms I don't think this is true for Coq. Ultimately, Coq relies on a type/inhabitant separation. When you spoke of Coq as a programming language, the terms you can always "run" are only the inhabitants. > So it is extremely unclear to me that the distinction you are making is fundamental. I don't know if it is entirely binary, but it is sufficiently precise for useful terminology. A programming language is a language that can be used for programming, namely it is a language whose every term can be mechanically interpreted in an "efficient manner." > dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well I don't think that any existing dependently typed languages do anything particularly effectively (neither programming nor specification), but that is beside the point :) It is certainly possible to combine a specification language and a programming language, but not without some formal delineation or the experience would be frustrating (i.e., it is possible to interpret some subset of TLA+ terms, but I am not sure it can be syntactically easy to determine which). This is, however, something that TLA+ tries hard to avoid as a design principle, because we do not yet know of any feasible way to scale specification from the "program level" to arbitrary levels of interest. Unlike Coq, TLA+ was designed not as a research tool for logicians, but as an industrial-strength tool for practitioners (I wrote about the design principles behind TLA+ in part 1 of my series: https://pron.github.io/tlaplus https://pron.github.io/tlaplus).