The invocation of Church's thesis is not a religuous move but rather a warning to the reader that the author is describing informally an effective procedure which could be translated into a construction of a Turing machine (if one enjoyed such a thing). This is completely standard in computability theory.

We could ask whether we have to worry about the informal level of proof or Church's thesis itself. The answer is that Church's thesis has been tested billions of times in practice: every time anyone thinks of an algorithm and then actually codes it up, that is a confirmation that they did not violate Chuch's thesis and that their sense of what makes an algorithm did not lead them astray. In any case, for the paranoid there is always the formalization of Halting problem.

The invocation of Church's thesis is not a religuous move but rather a warning to the reader that the author is describing informally an effective procedure which could be translated into a construction of a Turing machine (if one enjoyed such a thing). This is completely standard in computability theory. (And other branches of mathematics have a similar level of rigour, as pointed out by Jason Rute in the comments.)

We could ask whether we have to worry about the informal level of proof or Church's thesis itself. The answer is that Church's thesis has been tested billions of times in practice: every time anyone thinks of an algorithm and then actually codes it up, that is a confirmation that they did not violate Chuch's thesis and that their sense of what makes an algorithm did not lead them astray. In any case, for the paranoid there is always the formalization of Halting problem.