[sfvisser]

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.

[smadge]

That’s true but in most languages the things you prove are relatively obvious propositions like “(A and A)implies A.”