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