Does the law of the excluded middle imply the existence of "intangibles"?

With LEM there is a very simple (but extremely long) proof that there exists a shortest program, in some fixed computer language, that prints the first million questions on Stack Overflow.

For a string of that complexity, no reasonable foundational system for mathematics, such as ZF set theory, can determine an optimal program or its length. Valid theorems of the form "the minimum program length is 1267301" or "the following program [...code...] is optimal" are not provable in ZFC once the shortest program for the string is significantly longer than a program describing ZFC.

The consequence is that LEM and very little additional logical strength show that a shortest program "exists", but proving that a particular program is the object that was shown to exist is impossible even in very strong systems of axioms for mathematics.