271–280 of 288 posts
I don't know who the target audience was, but I found the lecture very confusing and the message really badly passed (he keeps talking what is already written in the slides, etc.). I had to play it at 1.6x the regular speed so I could move on with it. Regarding the topic, I think there are multiple ways of expressing ideas, where math happens to be just one of them. For instance, for the Greatest Common Divisor examp…
I don't know who the target audience was, but I found the lecture very confusing and the message really badly passed (he keeps talking what is already written in the slides, etc.). I had to play it at 1.6x the regular speed so I could move on with it. Regarding the topic, I think there are multiple ways of expressing ideas, where math happens to be just one of them. For instance, for the Greatest Common Divisor examp…
gcd x y | x == y = x
| x > y = gcd (x - y) y
| otherwise = gcd x (y - x)
Earlier quoted context omitted.
> As a result, primarily in the U.S., the topic became prematurely known as "computer science"---which actually is like referring to surgery as "knife science"---and it was firmly implanted in people's minds that computing science is about machines and their peripheral equipment. Edsger W Dijkstra. Mathematicians and computing scientists: The cultural gap. Abacus, 4(4): 26–31, June 1987. ISSN 0724-6722. URL http://dl…
In the SICP lectures, they explain why names like 'Computer Science' come into being. They explain it by explaining the origins of the word 'Geometry', which translates to 'Earth Measurement'. What they deduce is when a field is young, its hard to make a distinction between the science behind the field and instruments/tools you spend time with to make the science happen. That is because you spend so much time with th…
It is also the official term for computer science in many cultures. Mostly in European countries/languages.
Earlier quoted context omitted.
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…
> 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 en…
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+.
Earlier quoted context omitted.
>Honestly I think it might be time to phase out teaching imperative and object-oriented programming. I have seen plenty of universities teach Java and C++, haven't seen any that teach actual OOP. James Coplien aptly calls the current paradigm "class oriented programming".
It triggers me to no end when I watch an introductory course, for people with no previous exposure to any programming language, and the teacher starts with "public static void main()" In order to understand it, you need to have a good grasp of classes, static methods, access controls. This is usually followed up by a request to ignore the entire line, which is one of the worst habits you can have as a developer. Then…
One of the first CS courses at University was OOP in Java. I really struggled to grasp OOP, for most of the first year. It didn't "click" until I tried doing it in Python; after that I went down the rabbit hole into meta-object protocols, Smalltalk/Self/Newspeak, etc.
Java seems to occupy the opposite of a sweet spot: it makes learning difficult for newcomers, yet it's very limited and restrictive for those with experience. Not only is it overly verbose and ceremonious compared to untyped languages like Python, but also compared to ML/Haskell, whilst being less expressive and less safe!
Earlier quoted context omitted.
> 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 en…
> 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). Secon…
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).
Don't have the chance to watch the video but highly disagree with the title. Math as a language is just a DSL which carries a lot of historical burden that is not friendly at all. Programming languages can achieve same level of abstraction with more clarity. Math instead added too much specific syntactic sugar(bad is multiply(b, a, d), log a is log(10, a) or log(e, a)), operator overload (/ for divide and dy/dx for d…
The talk is about TLA+, which is somehow not a programming language, yet you follow a syntax and describe algorithms and then I'm not sure what happens. Maybe you prove your algorithms and call it a day, or maybe you can ask your program to run it, like an external dependency. It's very unclear how TLA+ is neither programming or how it fits in with your programming. But he is not asking you to do normal math notation…
You can do that, or check it with a model checker (which is much easier). Either way, you verify your algorithm rather than "run" it (although the model checker lets you simulate or "run" a random execution).
Earlier quoted context omitted.
Sure, everyone is enthusiastic about their tools. Still, it is not telescopes that are the subject of the science of astronomy.
It's not the subject, no, but the limitations on telescopes are what places limits on how much astronomy can do, and by improving their telescopes, and by improving how they use their telescopes, they can find out more than what they could before.
Earlier quoted context omitted.
> 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). Secon…
> 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 ty…
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).