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

[Freek Wiedijk]

Dear Talia and others,

Of course there is no inherent meaning to the word "program".
It depends on the person what they mean with it.  Also it's
a bit like Wittgenstein's analysis of the notion of "game".
These concepts are not very precisely delineated, there
is just a social consensus based on how the word is used
in general.

For me a program is something for which there is a notion of
time evolution.  I.e., if there is a notion to be denoted by

   ->
   
a notion of taking steps.  In type theory that's term
reduction, in operational semantics it's state transition,
the physical state of every processor continuously evaluates
through time too, hell, even a Turing machine takes steps.
So the notion of time is for me the essential ingredient:
in time a program makes progress towards something that it
is supposed to accomplish.

Of course, a value already is a finished result, so that's
a trivial program that won't take any steps anymore: but
still it can be in a domain for which such an arrow exists,
and then it still counts as a program to me too.

We have various things;

  - terms
  - proofs
  - programs
  - states

I guess Talia's question is what inclusions between these
notions we think are natural.  I don't see any obvious
inclusion in any direction myself, but I guess others
will disagree.

Also (I think this already was asked, but I would like to
repeat it): the original question was whether every proof is
a program, but from discussions with Dan Synek I remember
the question: can every program (in the general sense)
be seen as a proof?

Freek