4 ms·

> No, I mentioned it before, and my point isn't about linear time in particular. If you write a specification of an algorithm of time complexity T(n), the expec

> No, I mentioned it before, and my point isn't about linear time in particular. If you write a specification of an algorithm of time complexity T(n), the expectation is that interpreting the algorithm would take O(T(n)). This is what I mean by "efficient". What algorithm? There are many algorithms that inhabit the same type. A specification that's detailed enough to be able to analyze its complexity is usually a program... and it's easy to write a program that runs in linear time in Coq. > That doesn't matter. I can specify a function by giving it a type -- say it's a function from the naturals to their Goldbach pairs. Turning this into a program requires finding a lambda term that computes such a function. In Coq, you cannot specify a function by giving its type. First, CiC is not an extensional type theory in general; it cares about how things are computed, not just what the answer is. Secondly, for many interesting function types in Coq, there are an infinite, or even uncountable, number of inhabitants (for example : Prop -> bool). Moreover, in Coq's core type theory, even if it could automatically find all lambda input-outputs pairs that inhabited some type, that would not be justification to replace the quantified type (you need to assume the function extensionality axiom if you want this). > I didn't say there was. What I said was that a type in Coq is not a computation, and a computation is not a type. Just as a proof is not a proposition and a proposition is not a proof. A type in Coq is no more or less a computation than a term is. I don't understand what this has to do with "specification vs programming." As for "a proposition is not a proof", I think that is the main point of significant disagreement between us. Why do you think True doesn't prove Prop, for instance? It may not be the most interesting proof in the world, but neither is the proof I of True (and in many cases, proofs of Prop are very interesting in themselves, particularly in the context of dependent elimination). > In TLA+ there is no such distinction. You cannot talk about a program that computes that function, but always the set of all programs that do (i.e., just the type). Okay, then neither of them have such a distinction. What you seem to be missing is that in Coq, the mechanism for manipulating types is not different from the mechanism for ordinary program evaluation; it looks like TLA+ uses an axiomatic formulation rather than computation rules, so if you were to add evaluation to TLA+ you'd probably need a new set of semantics, but that's not the case for Coq. > I am not talking about writing an algorithm to solve such a problem automatically, but about a programming language that always does so. As you noted, such a programming language is impossible, so I don't understand why you are talking about it. The impossibility of that hypothetical programming language doesn't mean you can't write a single unified programming language (without two different "parts") that also functions as a specification language, and I genuinely don't understand why you think it does. > They have been an abysmal failure when it comes to synthesizing anything that could be considered a replacement for programming. The state of this has been steadily improving! 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.

pron 8y ago
> 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)

pron 8y ago

> 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)