The progress in computer programming leads to the shift in traditional correlation between intuitive and formal components of mathematical knowledge. From epistemological point of view the role of intuition decreases in compare with formal representation of mathematical structures. The relevant explanation is to be found in D. Hilbert’s formalism and corresponding Kantian’s motives in it. The notion of sign belongs to both areas under consideration: on the one hand it is object of intuition in Kantian de re sense, on the (...) other hand, it is part of formal structure. Intuitive mathematical knowledge is expressed by primitive recursive reasoning. The W. Tait’s thesis, namely, that finitism as methodology of mathematics is equivalent to primitive recursive reasoning is discussed in connection with some explications of Kantian notion of intuition. The requirements of finitism are compared with normative role of logic. (shrink)