[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
If we are asking `what is a program' without further qualifications, then I believe the discussion so far has been too `procedurally' focused, leaving out a class of programs and programming languages. For example, Prolog is a programming language -- its name says so (and so does Wikipedia). A Prolog program is a sequence of clauses and a query, asking if some new clause is a consequence of the others. The answer is no or yes (perhaps with some more information). There is no inherent notion of time, or reductions. One may say: but the answering the query is performing a sequence of SLD resolutions. Well, nowadays -- no. First, in answerset semantics, a Prolog program is just an easier-to-read SAT solver query. Second, for a long time Prolog has supported constraints over various domains (beside the equality constraints over terms, of course). So, at some point an execution engine might consult a constraint solver. Some constraint solvers are built-in. Some are external: there are constraint-logic programming systems (CLP) that consult an SMT solver. In principle an execution engine may even consult with the user (e.g., via a debugger interface). This is all called programming -- that's what the last letter in CLP stands for. Seeing as more and more bona fide programming languages are interfacing with Z3, perhaps it is not a stretch to call an SMT query a program. Or a query of a theorem prover. (And although I prefer not to go into that direction, I have seen several presentations advertizing machine learning as programming. In that case, it is really very hard to tell how the answer is arrived at. Still, some people do call training a neural net and then querying it programming. So a program is a set of training data and a query.) A small remark on Neel Krishnaswami's approach: > 3. A language is a *programming language* when you can give at least > one model of the language using some machine model. Well, let's take as a model of a language a term model -- which surely exists if the language/algebra has constants/generators and equalities are algebraic identities. (actually, the overall point holds for more general identities). That is, the carrier set of the algebra is just a set of terms quotiened by equalities. By `give a model using some machine model' I understand I need to present a machine that given a term produces some element of the carrier set. Since these elements are term equivalence classes, and a term itself is a representative of its class, our machine is the identity. I believe it is physically realizable. Thus every language (a generalized algebraic theory) is a programming language?
