This talk aims to provide a philosophical analysis of the notion of "proof by Church's Thesis", which is - in a nutshell - the conceptual device that permits to rely on informal methods when working in Computability Theory. Thus it allows, in most cases, to not specify the background model of computation in which a given algorithm - or a construction - is framed. In pursuing such analysis, we carefully reconstruct the development of this notion (from Post to Rogers, to the present days), and we focus on some classical constructions of the field, such as the construction of a simple set. Then, we make use of this focus in order to support the following encompassing claim (which opposes to a somewhat commonly received view): the informal side of Computability, consisting of the large class of methods typically employed in the proofs of the field, is not fully reducible to its formal counterpart. That is to say, informal constructions typically refer to a kind of objects that are: 1) not extensionally fixed; 2) independent from any specific formal model.