In , types and propositions, programs and proofs, all use the same syntax. But proving a proposition and implementing a program are still different activities. We can give orders or recite poetry in English, but are orders and poems the same because they share the same language, sometimes even the same sentences?

I think the main difference between programs and oroofs in coq is that in proofs, if you have two things of type T, you don't care which one is used, as long as the type is correct. In programs, you do care.

Sign in to participate in the conversation

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !