[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
