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

[Talia Ringer]

Hi friends,

I have a strange discussion I'd like to start. Recently I was debating with
someone whether Curry-Howard extends to arbitrary logical systems---whether
all proofs are programs in some sense. I argued yes, he argued no. But
after a while of arguing, we realized that we had different axioms if you
will modeling what a "program" is. Is any term that can be typed a program?
I assumed yes, he assumed no.

So then I took to Twitter, and I asked the following questions (some
informal language here, since audience was Twitter):

1. If you're working in a language in which not all terms compute (say,
HoTT without a computational interpretation of univalence, so not cubical),
would you still call terms that mostly compute but rely on axioms
"programs"?

2. If you answered no, would you call a term that does fully compute in the
same language a "program"?

People actually really disagreed here; there was nothing resembling
consensus. Is a term a program if it calls out to an oracle? Relies on an
unrealizable axiom? Relies on an axiom that is realizable, but not yet
realized, like univalence before cubical existed? (I suppose some reliance
on axioms at some point is necessary, which makes this even weirder to
me---what makes univalence different to people who do not view terms that
invoke it as an axiom as programs?)

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.

Talia