[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Anyways, it just feels strange to get to the last three weeks of my
> programming languages PhD, and realize I've never once asked what makes a
> term a program 😅. So it'd be interesting to hear your thoughts.
I think it's not a property of the object but has instead to do with
the intent. When I write a proof, it's a proof (and probably a broken
one as long as I haven't mechanically checked it), and when I decide to
try and run it then it becomes a program.
Stefan
