The identity of proofs
Here we may consider the lambda-calculus, with certain notions of reduction, as the programming language.
But this is certainly wrong: a normal lambda-term corresponds to the output of the computation, and we do not want to identify algorithms only by their input-output behaviour.
It would seem that Gentzen's proof-theory has not become yet a theory of proofs: we do not know yet how to identify its objects.
One attractive feature of such a semantics is that it would allow us to define the notion of identity of proofs and also of (sequential) algorithms. Also for this reason a philosophical investigation of recent development in game-theoretic semantics seems urgent.