That's because proof calculus (such as natural deduction) specifies how parts of a logic formula can be manipulated without changing its meaning. It's easier to

That's because proof calculus (such as natural deduction) specifies how parts of a logic formula can be manipulated without changing its meaning. It's easier to prove and maintain the universal correctness of underlying mechanics that way. As for functional programming, ML (the Meta Language, where the object language is HOL or Higher Order Logic https://en.m.wikipedia.org/wiki/ML_(programming_language) https://en.m.wikipedia.org/wiki/ML_(programming_language) ) was created in 1973 for manipulating proofs. C was created in 1972.