But programs are proofs! At least in the light of the Curry–Howard correspondence. :) Anyways, I do agree that in programming it’s easier to see what are intr

But programs are proofs! At least in the light of the Curry–Howard correspondence. :) Anyways, I do agree that in programming it’s easier to see what are introductions, assumptions, definitions, functions, values etc. You can’t just invent a notation and go with it. Everything needs to be defined from the ground up. It’s constructive and I like that, probably because I’m a programmer.