5 ms·

> 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

> 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. Firstly, yes, it is absolutely true for Coq (or at least, a large subset of it). The set model is essentially the entire basis for CiC's claim to consistency. I'm fairly sure TLA+ also has such a model (somewhere). Secondly, all terms in Coq, including types and universes, are inhabitants of some type, so there is no distinction between "the inhabitants" and all Coq terms (it's true that weak head reduction leaves products and other obvious types alone, but that's not the case for stronger forms of reduction like strong normalization, or for full conversion). Moreover, the conversion that occurs in the static phase (typechecking) has the same semantics as the execution during the dynamic phase (runtime). So I really don't understand what you're driving at. > 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." "Efficient manner" is pretty vague. I suspect there are widely used programming languages that will differ by 3 or 4 orders of magnitude while evaluating semantically identical expressions, while nonetheless both clearly being programming languages. Besides, many optimizations are only optimizations for certain data distributions, and if the compiler guesses wrong it can hurt performance; but that doesn't seem to me to have anything to do with whether something is a programming language or not. If all you care about is the default reduction, Coq's certainly tries to be fairly efficient: beyond optimizing the usual lazy reduction, it exposes many other reduction strategies, tuning knobs to tweak how reduction runs to improve performance when domain information is available, and even contains multiple implementations of some reduction strategies so people can select the appropriate one for their use case. > I don't think that any existing dependently typed languages do anything particularly effectively (neither programming nor specification), but that is beside the point :) I'm well aware of your biases here. Regardless of their origins in PL research, plenty of useful work has been done in dependently typed languages, including much larger developments than any I'm aware of in TLA+. I'm not really interested in arguing their relative merits--clearly, both are useful--I'm just asking you not to pretend to make general statements about programming languages while actually talking about TLA+.

pron 8y ago
> The set model is essentially the entire basis for CiC's claim to consistency. I am not saying that types do not have a set model, but that types and inhabitants are fundamentally separate. Or, put another way, a lambda term specifies a single (parameterized) execution (up to evaluation strategy), and that is the only thing that can be made to "run" (I'm sure there are ways to extract, say, a sole inhabitant of a type, but types cannot in general be turned into executable programs). > "Efficient manner" is pretty vague. I suspect there are widely used programming languages that will differ by 3 or 4 orders of magnitude while evaluating semantically identical expressions, while nonetheless both clearly being programming languages. I'm talking about exponential differences in time complexity, or even infinite ones. You can easily specify "computations" with infinite (or even uncountable) nondeterminism in TLA. > I'm just asking you not to pretend to make general statements about programming languages while actually talking about TLA+. My (and I think, Lamport's point) is that there is a fundamental difference between a specification language and a programming language. It is certainly possible to mesh the two and call the result "one language", but then it must necessarily contain two deductive systems, and so I think the distinction can still be made. Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner. So whether it's two languages or one, there is a fundamental difference between those expressions that can be used for programming (little nondeterminism/use of quantifiers) and those that are necessary for specification (unrestricted nondeterminism/quantifiers).
- Jweb_Guru 8y ago
  > I'm talking about exponential differences in time complexity, or even infinite ones. You can easily specify "computations" with infinite (or even uncountable) nondeterminism in TLA. SQL joins are worst-case exponential in the number of relations joined, where n = the total number of rows in the database (though there are many special cases that can help reduce this). I believe many people nonetheless consider SQL a programming language--with WITH RECURSIVE, it is Turing-complete. You could probably talk me into believing it's more of a "specification language," but despite that people use it for performance-critical things (admittedly usually in one of the special cases where it's better-than-exponential, but such special cases exist for most intractable problems; it doesn't seem to me that the nature of the language can be thought to fundamentally change depending on the data set). > Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner. I specifically object to this! Coq executes what you term the specification parts in a very different way than trying to exhaustively enumerate solutions--one that is actually quite efficient and can be mechanically executed. Essentially, rather than trying to eliminate the quantifier, it tries reducing the type, and the body bound by it. A key point is that this mechanism isn't special-cased for the "specification" parts--it's exactly the same reduction mechanism used everywhere in the program, and indeed it's very important for conversion that reduction behave this way. Thus, you can indeed efficiently, mechanically execute a type in Coq. Once it reaches normal form, of course, you can't perform any more reduction--but from the Coq kernel's perspective, up to eta conversion, types in normal form are distinct from an enumeration of all their inhabitants, meaning it is indeed doing the right thing here. In other words: Coq does not allow you to only program with non-type terms, and it doesn't make a clean distinction between inhabitants of types and types themselves. Moreover, while for quantified parts this isn't usually that interesting, for nondeterministic parts (such as match expressions on unknown variables) it can actually be quite important; for example, dependent elimination within the return type of a match clause can determine the index of a value of an inductively defined type, thus actually affecting program execution (and vice versa, of course; for instance, a type can be constructed representing n iterated lambdas, where n is an unknown value that may either be specified at runtime or at compile time. It is this latter case that gives rise to techniques like proof by reflection that may approximate an exhaustive search in order to produce a proof object--but they do so because the user wrote a program specifically to do exhaustive search, not because there's some exhaustive search mechanism built into the language).

pron 8y ago

> The set model is essentially the entire basis for CiC's claim to consistency. I am not saying that types do not have a set model, but that types and inhabitants are fundamentally separate. Or, put another way, a lambda term specifies a single (parameterized) execution (up to evaluation strategy), and that is the only thing that can be made to "run" (I'm sure there are ways to extract, say, a sole inhabitant of a type, but types cannot in general be turned into executable programs). > "Efficient manner" is pretty vague. I suspect there are widely used programming languages that will differ by 3 or 4 orders of magnitude while evaluating semantically identical expressions, while nonetheless both clearly being programming languages. I'm talking about exponential differences in time complexity, or even infinite ones. You can easily specify "computations" with infinite (or even uncountable) nondeterminism in TLA. > I'm just asking you not to pretend to make general statements about programming languages while actually talking about TLA+. My (and I think, Lamport's point) is that there is a fundamental difference between a specification language and a programming language. It is certainly possible to mesh the two and call the result "one language", but then it must necessarily contain two deductive systems, and so I think the distinction can still be made. Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner. So whether it's two languages or one, there is a fundamental difference between those expressions that can be used for programming (little nondeterminism/use of quantifiers) and those that are necessary for specification (unrestricted nondeterminism/quantifiers).

Jweb_Guru 8y ago
> I'm talking about exponential differences in time complexity, or even infinite ones. You can easily specify "computations" with infinite (or even uncountable) nondeterminism in TLA. SQL joins are worst-case exponential in the number of relations joined, where n = the total number of rows in the database (though there are many special cases that can help reduce this). I believe many people nonetheless consider SQL a programming language--with WITH RECURSIVE, it is Turing-complete. You could probably talk me into believing it's more of a "specification language," but despite that people use it for performance-critical things (admittedly usually in one of the special cases where it's better-than-exponential, but such special cases exist for most intractable problems; it doesn't seem to me that the nature of the language can be thought to fundamentally change depending on the data set). > Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner. I specifically object to this! Coq executes what you term the specification parts in a very different way than trying to exhaustively enumerate solutions--one that is actually quite efficient and can be mechanically executed. Essentially, rather than trying to eliminate the quantifier, it tries reducing the type, and the body bound by it. A key point is that this mechanism isn't special-cased for the "specification" parts--it's exactly the same reduction mechanism used everywhere in the program, and indeed it's very important for conversion that reduction behave this way. Thus, you can indeed efficiently, mechanically execute a type in Coq. Once it reaches normal form, of course, you can't perform any more reduction--but from the Coq kernel's perspective, up to eta conversion, types in normal form are distinct from an enumeration of all their inhabitants, meaning it is indeed doing the right thing here. In other words: Coq does not allow you to only program with non-type terms, and it doesn't make a clean distinction between inhabitants of types and types themselves. Moreover, while for quantified parts this isn't usually that interesting, for nondeterministic parts (such as match expressions on unknown variables) it can actually be quite important; for example, dependent elimination within the return type of a match clause can determine the index of a value of an inductively defined type, thus actually affecting program execution (and vice versa, of course; for instance, a type can be constructed representing n iterated lambdas, where n is an unknown value that may either be specified at runtime or at compile time. It is this latter case that gives rise to techniques like proof by reflection that may approximate an exhaustive search in order to produce a proof object--but they do so because the user wrote a program specifically to do exhaustive search, not because there's some exhaustive search mechanism built into the language).