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

[Talia Ringer]

>
> For example, if I write a proof in Agda, using function extensionality,
> is it a program? No. But if I write --cubical in the header of my Agda
> program and import a suitable cubical library, then yes. I can define an
> integer using function extensionality so that Agda will get stuck trying
> to compute it but Cubical Agda won't (and I have done it in the cubical
> library as an illustrative example).


No wrong answers here, but I'm curious: What makes a proof in Agda using
functional extensionality different in your mind from a function that takes
a proof of functional extensionality as an input, and then returns the
proof? Is the latter a program? Is the latter a program once you turn on
--cubical, since now it has inputs? Do programs need to have realizable
inputs?

To my knowledge, a proof is a very (very) specific kind of program.
>

 What makes it more specific? In my mind, you can certainly view any
program in any language as a proof in some logical system, even if the
logical system is not actually implemented as the language's type checker,
and even if the corresponding logic is unsound. A proof in an unsound logic
is still a proof, I think---just a possibly useless one (possibly useful,
though, since you can have incorrect assumptions and still sometimes prove
things that in no way rely on them).

On Tue, May 18, 2021 at 2:10 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
>
> On 18/05/2021 21:58, Martin Escardo wrote:
> > (and it is
> > probably independent).
>
> In univalent type theories.
>
> Martin
>
>