even in Curry-Howard systems, x = x still holds “axiomatically” (in the sense relevant to your distinction).

This is not true. Curry-Howard systems are Turing complete. Turing machines are generalized as Lambda calculus which is basically search-and-replace ( https://en.wikipedia.org/wiki/Regular_language ). As such the “law” of identity is not fundamental e.g it’s not required for the logic-system to remain functional because all symbols can be interpreted contextually.

Demonstration is here: https://repl.it/@TodorGenov/Identity

In a constructive realm this is a proposition, not an axiom: **A = A => True**

Which is effectively the standard form of Hilbert’s Entscheidungsproblem and so there is a procedure (algorithm) to determine the correct answer.

Now, of course - any bit-wise comparison of infinite-length information streams will produce “True” as the result, but what you are ignoring is that comparing a stream of 1 bit and comparing a stream of infinite bits takes infinitely more time. Hence work.

Whereas x = x assumes it true axiomatically and ignores the cost-of-work. Time.

Instead, you must study the formal definitions and reason on those.

Indeed. Computer science is the study of formal systems. It all stems down from the Chomsky hierarchy.

I have been studying and practicing it for most of my life.

Unless, of course, you think Mathematics is exempt from being classified as a formal language?

The problem here is that “proofs compute” is ambiguous shorthand for a very specific mathematical statement, and you seem to misread the shorthand because it is ambiguous.

It may be a very ambiguous mathematical statement, but it is a very unambiguous and precise computer science statement. A **halting algorithm** which produces the correct result.

And all I can do to demonstrate to you the error in ignoring the amount of work required is this Gedankenexperiment. Look at these two (in?)equalities:

1 = 1

888888888888888888881 = 88888888888888888881

Notice how the truth-value of the first one is trivial to determine, but the 2nd one is harder for your brain.

x = x is actually an algorithm: equality(A,B). What you are really doing on a Turing machine is

A = 888888888888888888881

B = 88888888888888888881

( Observe how it got really easy to determine that A !=B when you compared their length? )

equality(A,B) => False

Assuming x = x is an error. You are taking infinite time(required to iterate over an infinite set) for granted.

Alas - this discussion will quickly devolve to Ultrafinitism.

The mathematics may be right, but the physics and the computer science doesn’t make sense…

And as history has shown us, the three fields are conjoined at the hip…

Computation is all about decidability. To ignore decidability while speaking about Curry-Howard is to speak of square circles.