[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
