[jtc1983]

These quotes from Girard are great, as is the mention of Frege below.

Typically, the objects related by equality can be thought to have the same meaning with respect to extension and different meanings with respect to intension. Further, the difference in intension reveals something of the computational content of the extensional object being referred to.

Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory. Both of these topics give one some insight on the relationship between the computational content of mathematical objects and how this content pertains to the question of whether two objects are “the same.”

Finally, I did skim the article itself and found it lacking. The author seems to be aware of the fact that there are surprising, highly non-trivial properties of the (seemingly trivial) notion of equality in mathematics. And also to be aware of the fact that the use of ‘=‘ in CS contexts isn’t some sort of abuse of notation. But there seems to be very little of interest here beyond some circumstantial verification of these two general (and well-known) facts about equality in the mathematical and computational contexts.

[lou1306]

> Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory.

Thanks! For the interested, Girard's book focuses on the Curry-Howard isomorphism, another great result linking computer programs (actually, the typed lambda-calculus) to mathematical proofs.