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

[Stefan Monnier]

> 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