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

[Martin Escardo]

This will not answer your question (which seems more philosophical than
mathematical).

The BHK / CH interpretation of logic applies equally well to classical
mathematics if we understand the imprecise notion of procedure as
function (for example, the classical set-theoretical notion of function).

Classical mathematicians using Lean apply this everyday in their
practical formalization work (for example).

What counts as a program, in my view, is subtle and so your question is
very appropriate.

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).

A term has a meaning for you and me (probably not exactly the same
meaning), and it may also have (or have not) an operational meaning to
the computer.

To make things worse, you may have contradictory realizable statements.
For example, each of ¬¬LPO and "all functions are continuous" are
realizable, but not simultaneously.

(LPO means "every sequence s:N->N either has a 1 or is constantly zero".)

Sorry for adding more to the confusion.

For more confusion: in the setoid model of type theory, countable choice
is just true. In the cubical model it is not provable (and it is
probably independent).

Martin



On 18/05/2021 20:42, Talia Ringer wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe