7 ms·

The assertion here seems to be that TLA+ isn't a programming language? I'm not sure that makes sense to me.

• pron 8y ago
  It most certainly isn't. It is generally impossible to interpret/compile a TLA+ algorithm efficiently (i.e. as a program that runs with similar complexity to the algorithm) because of the inherent nondeterminism in TLA+. OTOH, it is precisely this nondeterminism that allows you to use TLA+ to describe any algorithm/system at any level of detail. In fact, you can show that a language with similar descriptive power to TLA+ cannot be a programming language, and that no programming language can have a similar descriptive power (you could embed a specification language inside a programming language, but then you arguably have two languages).
  • 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).