[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The idea of computation being related to proof requires that there be some directional relation between proofs which can be used as a reduction relation. Without such a notion, then the terms that form a proof are entirely static. Many "reasonable" relations between proofs - i.e. those that preserve the final logical statement while retaining a valid proof, might not "reduce" to some "value" either. They could instead relate the proofs in such a way that the structures always get more complex (perhaps cut-introduction?). Would that still be a programme? But perhaps the question should be taken the other way around. Is every programme the proof of something? And if so what? We can fix the reduction relation with our operational notion of our programme, but then we're left wondering what properties we are computing. We can easily equip a programme with properties which are abstract enough that it will compute that property. But there are nots of properties which may hold of the programme which we probably can not call the programme a "proof" of without somehow giving more elaborated information without which we will find the satisfaction of these properties by the programme is undecidable. This missing information for decidability would seem necessary to supply if we want it to constitute a "proof" or giving someone the programme and telling them to verify the proof would be rather cruel. Whichever way you look at it, while you can sometimes wedge programming into the CH, it seems unlikely that the CH covers everything we mean by proof. On Tue, 18 May 2021 at 22:42, Stefan Monnier <[email protected]> wrote: > [ 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 > >
