[griffzhowl]

Use of the word "mechanical" to describe formal reasoning predates computers.

Here's the first sentence of Godel's 1931 On formally undecidable propositions...

"The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules."

Leibniz had discussed calculating machines (and even thought about binary arithmetic being the most appropriate implementation), so the general idea probably goes back quite far

Edit: Oh, I guess by "late 1930s" you're referring to Turing's 1936 paper where he defines Turing machines, rather than actual electronic computers. Still, understanding "formal" as "mechanical" predates it.

[pron]

Yes, by Godel's time the notion of "calculability" was already at least intuitively grasped, and it was then that "formal" was understood to mean mechanical. Turing made the connection rigorous.

Leibniz spoke of "automatons" and dreamt of some sort of "thoughtless" reasoning, but I don't know if he had the right building blocks to even think of mechanisation as we could since the 19th century. E.g. here's how Leibniz tries to justify the utility of formal reasoning: "Our thoughts are for the most part what I call ‘blind thoughts’. I mean that they are empty of perception and sensibility, and consist in the wholly unaided use of symbols... We often reason in words, with the object itself virtually absent from our mind."

So he definitely had the right concept - which is why formal logic is so old - but not the right language that most people would intuitively understand today.

[griffzhowl]

Leibniz even invented a calculating machine. I didn't know he'd actually built one

https://en.wikipedia.org/wiki/Calculus_ratiocinator

[DougBTX]

Perhaps it has to be that way, the motivation to build a mechanical computer is based on the belief that computation can be mechanised.

[DonaldPShimoda]

It's not a "belief"; that's what computability is. This definition is the whole point of the work by Church and Turing that resulted in the lambda calculus and the Turing machine, respectively.