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

Stefan Monnier <[email protected]> Tue, 18 May 2021 16:39:52 -0400
Newsgroups gmane.comp.science.types
Message-ID <[email protected]>
[ 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