> A specification that's detailed enough to be able to analyze its complexity is usually a program... Not necessarily, and I would claim that it usually isn't,

> A specification that's detailed enough to be able to analyze its complexity is usually a program... Not necessarily, and I would claim that it usually isn't, but to see that you have to pay close attention to how algorithms and systems are specified. I give the example of the QuickSort algorithm at the beginning of this post: https://pron.github.io/posts/tlaplus_part3 https://pron.github.io/posts/tlaplus_part3 > In Coq, you cannot specify a function by giving its type. Of course you can; that's the meaning of the type -- it's just not enough to get a computation. That's precisely the point I was getting at. A specification is a description of something at some arbitrary level of detail, but languages that allow compilation -- i.e. programming language -- normally require a minimum level of detail for that to be possible. In a language like Coq, this requirement is a strict syntactic distinction between types and lambda terms. > First, CiC is not an extensional type theory in general; it cares about how things are computed, not just what the answer is. Precisely. This is absolutely necessary for a programming language, and undesired in a specification language. (BTW, in TLA, what and how is arbitrary, because the temporal logic lifts everything that in Coq is operational into the denotation) > A type in Coq is no more or less a computation than a term is. A type is not a computation. To "run" something, or to speak of the operation of something, that something must be a lambda term. > the mechanism for manipulating types is not different from the mechanism for ordinary program evaluation I know that (I don't know Coq, but I know a bit of Lean, which is similar, I think), but that doesn't matter. You can compute with types, but there is a strict distinction between the common form of nonderterministic specification -- types -- and actual computation (not types). > As you noted, such a programming language is impossible, so I don't understand why you are talking about it. Because we're trying to work out the difference between a specification language and a programming language. A programming language is one that, when it describes a computation, can always be interpreted efficiently in the sense I meant. A specification language should allow specifying computations at arbitrary levels of detail. I claim that a specification language cannot be a programming language and vice versa -- except if we had this magical language I described. What you can do, and Coq does, is combine two languages in one, but even then the result requires a delineation between a computation and a specification (arbitrary nondet). > For example, https://www.cs.utexas.edu/~isil/sypet-popl17.pdf https://www.cs.utexas.edu/~isil/sypet-popl17.pdf looks quite promising for everyday programming tasks. I honestly do like the research, but this is going from converting two atoms of lead into gold in a particle accelarator to five, or like saying that Olympic high jumpers are steadily improving in jumping all the way to the moon... This is another discussion, but I like the research and I like the practice, but I don't buy the claims that such improvements in research put changes to practice on the horizon. The gap is still huge, and I also think some of the research (especially in programming language theory) is done based on assumptions that completely fail in practice (I wrote about that here: https://pron.github.io/posts/people-dont-write-programs https://pron.github.io/posts/people-dont-write-programs)