Rigorous books on basic computability theory Are there books on basic computability theory in which the authors formally prove computabiltiy of functions? By 'formal proof' I mean writing down explicitly the corresponding turing-machine, or lambda-term or proof that the given function is partial recursive. I would like to avoid as much as possible Church-Turing thesis in my proofs. Which of these models of computation (turing-machines, lambda calculus, partial recursive functions) is the best for my purposes?
 A: Similar to @user21820's way, I recommend a classic textbook Computability and Complexity: From a Programming Perspective by Neil Deaton Jones. It introduce computability rigorously but in a very plain, alternative and elegant way.
In the beginning of this book, the author introduced a very simple WHILE language first and also gave the syntax and semantic of that language rigorously. For example the syntax is as below.

The WHILE language here is based on command and then is imperative, but its data is a binary tree structure. And we know that program itself is also data, so this settings are very convenient to unify program and data.
In the following chapter, basic background of programming language theory is given, such as interpreter, compiler, specifier and related concepts ...
Based on WHILE language, the author leads us to the beautiful garden of computability and complexity in a very special path.
For example, the universality of computing is introduced by a self-interpreter which is a program.

And also the core part of the proof for s-m-n theorem is also a program.

At least for me, this fascinating book is very elegant.
So you probably can use a program to describe your algorithm and then proof it through the formal semantic of the WHILE language.

*

*pdf file of the book from author's home page

*the page of the book in MIT press

A: But is it a good idea to "to avoid as much as possible Church-Turing thesis in my proofs"?
Take a book like Cutland's wonderful classic Computability: An Introduction to Recursive Function Theory. After page 68, he does repeatedly give "proofs by Church's thesis”, meaning that he gives informal but rigorous demonstrations that some function $\varphi$ is computable by a finite algorithmic procedure -- and then appeals to Church's thesis to conclude that the function is computable by your favourite technical definition of computability (by URM machine, Turing machine, whatever).
This way we get brevity. But much more importantly, we also get vastly increased understanding. If I give you a ten-line outline of an informal algorithmic procedure for computing $\varphi$ you'll understand why it is a computable function. If, to go the other extreme, I give you a 500 line list of Turing machine code that happens to compute $\varphi(n)$ for input $n$, then just staring at that is likely to give you no understanding at all!
And in the theory of computability it is understanding we are after!
A: Well, arguably the best way to do it completely rigorously would be to first set up a simple programming language L that supports:

*

*String variables (binary strings suffice).

*Basic string manipulation: concatenation, substring-test, equality.

*Basic control-flow: if, while, one instruction per line.

And show that any program in L can be translated to a TM (or to whatever base model you pick).
Then you bootstrap to a better language L2:

*

*Integer variables (unary encoding suffices if your target model is inefficient like TMs).

*Basic integer arithmetic: 0,1,+,−,·,< (defined as functions)

*Higher control-flow: for-loops, function-calls (using an integer to store a program counter and a string to store a call stack), nested operations (via temporary variables).

And now it is very easy to describe computable functions using programs in L2, while completely avoiding any kind of CT thesis usage.
It is also instructive to do this, and pedagogically expedient, because it concretely demonstrates how programs in real-world programming languages are clearly implementable as TMs.
That said, even after building L2 and using it for a while, eventually one would stop giving explicit programs in L2 and start giving just high-level descriptions of algorithms, since it would be clear that they can be implemented in L2. One should not consider this peculiar to computability theory, since it is the same in design and analysis of practical algorithms and data structures. Actual code is good to have, but cannot substitute for exposition of intuitive ideas.
A: I did something like this about six years ago. I will try to outline how I did it. First of all let me describe the base computation model (let's call it $A0$ for the rest of the post) I used. Also, note that I don't know much (or anything) about PL design or stuff like that, so this might be far from optimal.
The $A0$-programs have the following variables: (1) temporary variables: $\mathrm{t0}$,$\mathrm{t1}$,$\mathrm{t2}$,..... (2) input variable: $\mathrm{x}$ (3) output variable: $\mathrm{y}$. All variables take can only take on the natural number values $\{0,1,2,3,4,5,.....\}$.
Further $A0$-programs have the following four commands ($v$ and $w$ can be any variables): (1) $\mathrm{v:=0}$ (2) $\mathrm{v:=v+1}$ (3) $\mathrm{while(v!=w)}$ (4) $\mathrm{End}$. Hopefully the commands are kind of self-explanatory. The fourth commands is used in place of brackets (to mark the end of a loop). If you are more comfortable with brackets then you could replace it with $\{$ and $\}$. Note that if the brackets don't properly match the corresponding "while" commands then we declare the program to be syntactically incorrect. Secondly the assignment symbol $:=$ can be replaced with $=$, as long as the underlying meaning is understood. Finally $while(v!=w)$ can be re-written as $while(v \neq w)$. Ultimately it is just a check for non-equality (when equality is detected the loop is exited).
Also note that, for simplicity, we can assume that all variables (except the "input variable") have the initial value $0$.

Actually, to allow for multiple input variables I used input variables as: $\mathrm{x}$, $\mathrm{x1}$,$\mathrm{x2}$,$\mathrm{x3}$,$\mathrm{x4}$,.... . However, since often we are using a program computing a function in one variable, using $\mathrm{x1}$ in place of $x$ seems a bit much. That's why I kept the variable $\mathrm{x}$, clearly describing the conventions in  case of "name collision" of $\mathrm{x}$ and $\mathrm{x1}$.
Next, I added various features to the base $A0$-programs (and called the subsequent computational model $A1$-programs,$A2$-programs etc.). The absolutely main thing about adding any feature is this. In each case, after some work, it could be shown quite evidently that all of these can be implemented in $A0$-programs. When you add the feature you must know that there is a sure mechanical way to replace the program (using extra features) to the base $A0$-programs.  In fact, in most cases, it was quite clear that this "mechanical way" can actually be accomplished by some simple "variable-renaming and replacement" (hard to describe it precisely without lengthening the post much further).

Describing the whole list of features would make the post too long. Usually at a number of points more than one choice/convention is available (out of which we can adopt the one that seems more suitable).
Ultimately after all the features have been added, call the resulting computational model $B$-programs. Then I wrote suitable encoding/decoding functions and wrote all the usual functions that are required for implementation of lists, which are variables[as long as they are manipulated with suitable functions only] that can be thought of as holding an indefinite number of values.
Finally, using these $B$-programs, one can write a "universal program" of sorts. Let me explain in what sense. First we decide a convention on how to think of any $A0$-program as a single natural number (essentially  a bijection). When the number is given to our $B$-program as input, it first converts it interprets is as a list of commands (command-1 to command-4 described in the beginning of post). But as I mentioned not all $A0$-programs are syntactically correct (since the "brackets" or "end" commands might not match with loops properly).
So, first a check is performed for the $A0$-program being syntactically correct and then it is simulated on the specified input. The output of our $B$-program is also the same as the output of simulated $A0$-program on the specified input.

As an ending note, something similar to what I did I had read few years earlier in the first few chapters "Computability, Complexity and Languages" book. However, there a "goto" language with labels was used there. So, I tried to use a language that felt easier to use.
I think something similar can be done with "string manipulation" too instead of using "numbers". Though I haven't tried that.
I could link the corresponding documents where I did that but I do remember noticing a mistake or two when I had a look at them last time. To remove them completely I would have to examine them again. That's why I am a bit hesitant to link them here.
Edit: To add a few more details, here is how I wrote the encoding function: Suppose $x_1$ and $x_2$ are the input variables to our encode function and $y$ is supposed to be the output variable. Then we have three sub-cases: (1) If $x_1<x_2$ then we set $y:=(x_2)^2+(x_2+x_1)$. (2) If $x_1>x_2$ then we set $y:=(x_1)^2+x_2$. (3) If $x_1=x_2$ then set $y:=(x_1)^2+2 \times x_1$. That is it for "encode" function. Then I wrote two separate functions (each with 1 input variable) to extract "first" and "second" components.
For variables to represent lists I used repeated applications of the "encode" functions[with few conventions/defaults set up in place that do require some care] and then wrote a number of list manipulation functions that one may use. It does take some space to write all those functions. On the other hand, if one wants to use lists directly, I suppose they may be incorporated as some kind of "primitive" (perhaps alongside with usual integer variables) in the original $A0$-programs along with manipulation operations. Then that would remove the need of all the encoding to represent lists.
A: Martin Davis, Computability and Unsolvability is rigorous to a fault. He uses Turing Machines and later recursive functions to define computability and decidability. It might be written in the style you are looking for.
I found it incredibly precise from a technical/logical point of view. But I found it a difficult book, if you haven't seen the basic ideas already somewhere else.
