Dod Doron,
I read and enjoyed your paper "An enquiry concerning human (and computer!) [mathematical] understanding". But I think you are dancing around issues that come up over and over in constructive mathematics, and there is one paragraph where I think you are simultaneously being visionary and reactionary:
Most of mathematics, even logic, is done within narrow computational frameworks, sometimes explicit, but more often implicit. And what mathematicians do is symbol-crunching rather than logical deduction. Of course, formal logic is just yet another such symbolic-computational framework, and in principle all proofs can be phrased in that language, but this is unnatural, inefficient, and worse, sooo boring.
I think that this view of mathematics is important, but I also think this view of logic is outdated. In the 20s and 30s, to be sure, logic was just an ad hoc formalism that deviated grossly from mathematical practice -- and unfortunately, this is still what "formal logic" means in some circles. But Brouwer's intuitionism and more generally *constructive* logic were developed precisely to rule out the sort of meaningless statements you object to (without resorting to a finitary restriction...in other words, constructive logic makes clear what it means to prove something "for symbolic n") -- eventually this led to a more natural, computational notion of formal proof. Indeed, there are several full-fledged programming languages based on constructive logic, such as Coq (the language Gonthier used to prove the four-color theorem), in which proving a theorem is *the same thing as* writing a program. Moreover these programs are not exceptionally unnatural, inefficient, or boring -- there is not a gigantic difference between programming in, say, Coq and programming in Maple.
I also find the question of finding decidable/efficient ansatzes very interesting, and you might be interested in knowing that it shows up in "constructive topology". For example, there is an old result (again following ideas of Brouwer) that the Cantor space (= infinite sequences of bits, a.k.a. functions Nat -> Bit) is *exhaustible*, meaning that given any decidable predicate A on the Cantor space (i.e., a function (Nat -> Bit) -> Bool), you can decide whether A(x) holds for all elements x of the Cantor space. This might seem strange, since the Cantor space is uncountable -- it's related to the classical proposition that the Cantor space is compact. From the fact that the Cantor space is exhaustible, it follows that given any two predicates A and B on the Cantor space, you can decide whether A = B. There is a post about this (including code) here
Noam