[TYPES] What's a program? (Seriously)

[Oleg]

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?