The formal and informal proofs

Hello,
Is a system strictly formal when each and every of its parts is made
entirely explicit, i.e. when the computing model with which it is
identified is a register machine? I hope I am not being a disgrace, as
I have _luckily developed into not seeing a world besides logic, but
even the Turing machine (a formalism more explicit than e.g. the lambda
calculus) seems to be making use of ideas which only become explicit if
implemented as e.g. an x86 machine.

Merry Christmas and Happy New Year,
Tom

.