This allusion to intuitionism is somewhat obscure. Perhaps you can
elaborate on what you have in mind?
Intuitionism is the insistence that we do math without the excluded
middle and proceed by constructing proofs from what we know. It
refuses to posit entities which we know "must" exist by way of
excluded middle but which we can't construct.
[Some variants of intuitionism go to unwarranted extremes: I read an
article in the Journal of Symbolic Logic in 1972 which seemed to claim
that "big" numbers such as 100 factorial don't exist in the same way
small numbers exist: my response was to write an assembler program for
the old IBM 1401 to calculate the precise value of 100 factorial. It
was actually easy to do so without simulating extra precision because
the 1401 had a "variable length word".]
Applied to programming, intuitionism would insist that a program must
be constructed bug-free before we can say we know that one exists. And
whether the "program" is constructed using a programming language, or
using mathematical symbols as a written intuitionist proof, it is
going to have essences (meaning) and accidents (notation or an actual
automaton which is either a real computer or an abstract, but fully
described, automaton such as a Turing machine).
What Seebach claims implies that in formal automata, the professor
CANNOT draw a Turing machine on the board and explain that this shows
what computers do, since the professor's constructive proof (proof by
construction) is "only" a picture, and it might confuse the students,
who MIGHT think that on the job they will have to program Turing
machines.
Which is nonsense, and grievously insulting to professors, their
students, and education.
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus- Hide quoted text -
- Show quoted text -