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

[Gavin Mendel-Gleason]

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 <monnier at iro.umontreal.ca>
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
>
>