Human reasoning is never purely formal. I think it works mainly along the lines of the material inference described by Sellars and Brandom. But as Brandom pointed out in Between Saying and Doing, any given material inference can still be represented by a formal inference.
Direct brain-computer analogies don’t seem to me to yield much. On the other hand, the theory of programming languages does yield insights into the foundations of formal reasoning, and the foundations of formal reasoning may indirectly yield insights into the ways human reasoning works.
A case in point is the notion of compilation stages. All programs need to be compiled or interpreted to be run. Usually, this happens in multiple stages. At each stage, expressions in a more expressive language are re-encoded into operationally equivalent expressions in a less expressive language. It may seem counterintuitive that this is even possible, but it is essential to the way something intelligible to us can be made to “run”.
This tells us that operational equivalence and expressive equivalence are not the same thing, and it suggests an analogy for the way second nature relates to first nature. Operational equivalence can be preserved by substituting references for inferences. Something that can only be expressed at a higher level can nonetheless be executed at a lower level. Things that can only be expressed through human language and reason can provide the occasion for operational execution by a physiological mechanism. (See also Free Will and Determinism; Psyche, Subjectivity.)