The remark from Girard may not be so far from some things Wittgenstein said at this or that point. But it's not clear that Girard's remark means anything like that "logic is invented/designed by humans". For example, it might also mean something like what Wittgenstein wrote in the Tractatus:

We have said that some things are arbitrary in the symbols that we use and that some things are not. In logic it is only the latter that express: but that means that logic is not a field in which we express what we wish with the help of signs, but rather one in which the nature of the absolutely necessary signs speaks for itself.

If you trawl Girard’s papers you will find him saying at least these two things:

Logic is subjective.

Logic is implicit - will never be explicit.

“The symbol speaks for itself” is the notion of denotational semantics mathematicians use. I am in the camp of “symbols mean whatever you interpret them to mean”.

> Who invents the rules

Anywho is:

they could be someone with states of mind, bending over endless amount of paper, paging, writing and deleting symbols on them with their pencil for some time (or forever)

Otherwise how could anyone invent rules?

It would be so great to get out some general&universal results starting from this setup... ;)

"Computer" used to be a job description before it acquired its modern meaning...

https://en.wikipedia.org/wiki/Computer_(job_description)