Not every programmer can write any program with equal ease, can we? It depends on your knowledge of available primitives: programming languages, libraries. One

Not every programmer can write any program with equal ease, can we? It depends on your knowledge of available primitives: programming languages, libraries. One who knows OpenGL will have an easier time spinning a 3D model than another who parses log files for a living. Similarly, a graph theorist like yourself will find it easier to prove theorems of form 3. than the rest of us. (At least half of th. 2 seems easier though. Suppose N divides (N-1)!+1; none of 2...(N-1) divides (N-1)!+1; so none of 2...(N-1) divides N.) I guess the main confusing part about the Howard-Curry isomorphism is that the code / comment conventions are commonly reversed between proofs and programs. Programs show a sequence of actions, and may show machine state in the comments, e.g. ... x = x * f; //x now contains factorial(n) ... Proofs show state instead (i.e. the proposition that was proven so far), and may contain the operation in the comments: ... (x + y) ^ 2 = (x + y) * (x + y) Using the distributivity of addition: (x + y) ^ 2 = (x + y) * x + (x + y) * y ... In either case, you: - start with an initial state - choose a sequence of operations from an existing set - end up with a desired state If either your program or proof has bugs, there are certain initial states that will break some step in the operation sequence and cause an undesired final state.