Careful there. Source code to a program is also a fact; it's merely the proof of some statement in some theory. This is one way to view the Curry-Howard-Lambek

Careful there. Source code to a program is also a fact; it's merely the proof of some statement in some theory. This is one way to view the Curry-Howard-Lambek isomorphism. So, then, what is it about source code which would make it copyrightable again? Are systems like Metamath and Opentheory eligible for copyright or not? To me, the current copyright regime is what's "absurd" and "plainly ridiculous"; I am merely drawing conclusions based on what exists.