[ 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
