Knowledge vs Reason

[Ignacio Añón]

Caballero wrote:

"Let's consider an example of technology: a tablet in which it is
possible to write mathematical formulas, and they are automatically
transformed into expression in a programming language and executed.
Let's consider this machine, which I will refer to as "this tablet,"
from the point of view of Aristotle's four causes.....

...Now, my claim that the use of proof assistants in everyday
mathematical practice is not a fundamental problem, but a
technological one, can be reformulated in this framework as follows:
all the requirements for the material, formal, and final causes are
satisfied, but there is a requirement missing concerning the efficient
cause."

This reference to aristotle is interesting. He also liked, as the
presocratics, and Plato did, to distinguish between "Knowledge", and
"Reason". Rigourous, automated, detailed, step by step, verification
of given data, was for him tied to "Knowledge", while "Reason" was the
creative, holistic, grasp of an idea, what Harvey Friedman would refer
to as a "Jump".

The aristotelian distinction between Reason and Knowledge, was also
important for the Cartesians, Newton, Leibniz, and even for
mathematical skeptics like Goethe, and of course for Kant. The old
distinction between synthetic, and analytic, knowledge, came from
it...

Your enhancement of the Pi calculus, as a first experiment to build a
programming algebraic language worthy of our intuitive grasp, looks
very important, I will look into it; but most of the work done in
proof assistants, seems closer to the knowledge realm, than to the
Reason sphere...

Formal verification, will always be a secondary intellectual activity,
in my view. The prestige that "rigour" has in math and science, comes
from a subtler idea: it is based on the notion that our need for
certainty, should be perpetually enhanced by new insights; rigour per
se, and certainty, are a dead end otherwise...