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

[Sergey Goncharov]

Dear Talia,

I am not sure if I can say something particularly intelligent in matter terms, but in your post you are 
first asking if proofs can be seen as programs, and then switch to the question if "terms" can be 
regarded as programs. I am wondering why you have no issue with regarding "terms" as proofs, but you 
have an issue with regarding "terms" as programs.

To my knowledge, a proof is a very (very) specific kind of program. Exotic cases aside, let us take 
Haskell as an example. Its Curry-Howard logic is degenerate, but it is a programming language, isnt it?

Cheers,
Sergey

On 18/05/2021 21: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
>