If You're Not Writing a Program, Don't Use a Programming Language [video]

> I believe many people nonetheless consider SQL a programming language

Yes, but I don't think anyone considers a SQL join to be a description of a linear-time algorithm.

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

I never said you always need to exhaustively enumerate solutions. Nevertheless, the problem of extracting a computation from a specification (e.g., an inhabitant from a type) is undecidable in general[1]. Hence, specifications cannot be generally compiled, therefore they are not programming languages.

They could be a new kind of programming language, where some search algorithm could sometimes find a computation, but that would be a "programming language" in a completely different sense; Lamport does acknowledge that possibility (I know some people are researching program generation, but the results so don't look very promising, and in any event no one expects them to ever be more than heuristic, even if they're ever effective).

[1]: I'm not sure what happens if you know the type is inhabited. I guess it will be decidable in that case (just as finding a proof of a proposition that's known to be a theorem), but the search is still intractable, and there is no way the resulting computation would be efficient.

> This is the first mention either of us have had of "linear-time" outside of a discussion about specifications.

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 p(T(n)), where p is some polynomial (i.e. no exponential slowdown or worse). This is what I mean by "efficient".

> but that is not how Coq interprets types at all; from its perspective, types are terms of independent interest, and are moreover themselves inhabitants of some other type.

That doesn't matter. I can specify a function by giving it a type -- say it's a function from the even naturals to their Goldbach pairs. Turning this into a program requires finding a lambda term that computes such a function.

> There's no special notion of "finding an inhabitant" as distinct from normal program execution

What I meant was that a type in Coq is not a computation (although it could be the result of a computation), and a computation is not a type (although it could produce a type -- Pi types).

> I am not saying this is not a meaningful distinction in TLA+

In TLA+ there is no such distinction because you cannot talk about a program that computes that function, but always the set of all programs that do (you can, of course, give more and more detail to restrict the set, i.e., create subtypes, but there is no "the computation"); that set is always either empty or infinite. In fact, if it's non-empty, it's always too big to even be a set (it's a proper class).

> Sometimes executing it is tractable and sometimes it isn't, but I don't agree that writing an algorithm to solve such a problem automatically transforms your domain from "efficient, everyday programming" to "ineffecient, specification-driven programming."

I am not talking about writing an algorithm to solve such a problem automatically, but about a programming language that always does so.

> So I'd say these ideas have been a success, though hardly an unqualified one.

They have been an abysmal failure when it comes to synthesizing anything that could be considered a replacement for programming. But we're talking about two radically different measures of success. I'm talking about a commercial process of turning lead into gold, and you're talking about turning a couple of lead atoms into gold atoms in a particle accelerator.

> 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

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

I work on the formal verification of AI systems as well, but focusing on model-based reasoning systems rather than the model-free ML systems. What you've described is exactly what terrifies me most about ML in safety critical contexts: it can fail in a large number of ways, and predicting these ahead of time is generally intractable.

I like to think of it in terms of quantifiers: for most systems it's fine to say that there exists a set of representative tests that the system passes. For critical systems, you really want "for all" in there instead.

Fortunately the model-based systems are much easier to reason about, even if they suffer from difficulty modeling certain cases. For a model-free system I think the starting point would be to precisely state a correctness criterion that could be used as a decision procedure on the output of the model; the combined system would be "verified" to a certain degree. Unfortunately you can't guarantee that it would always be able to yield an answer (it might always give a bad one which was rejected) and, the more fundamental problem, one might reasonably expect that if you can express the correctness property to a sufficient level of detail that you can perform verification on it you might be able to write an easier-to-verify implementation that doesn't rely on ML.

This stuff is hard, yo.