In Sipser's book "Introduction to the theory of computation" there are 2 methods for proving that $\rm HALT_{TM}$ is undecidable by a reduction from $\rm A_{TM}$
I am trying to figure out the connection between these 2 methods.
Proving by contradiction. Assume there exists a TM $R$ that decides $\rm HALT_{TM}$ and construct TM $S$ to decide $\rm A_{TM}$
S="On input <M,w>: Run R on <M,w>, if R reject then reject if R accepts, simulate M on w until it halts Accept if M accepts else reject"I believe that this method is called "using a subroutine"(Am I right?)
The second method is mapping reduction: $\rm A_{TM} \leq_m \rm HALT_{TM}$. Here the proof is by creating a function that gets the encoding of a machine from $\rm A_{TM}$ and computes encoding for a machine for $\rm HALT_{TM}$
F="On input <M,w>: M' = "On input x: Run M on x If M accepts, accept If M rejects, enter a loop Output <M',w>"
It seems that the methods are completely different but in the book it says that the second method is just "more formal". I am trying to understand whether there is some kind of connection between the methods or that these are 2 different ways to prove undecidability.
I hope you can clear this up for me a bit.
You are right; these are two different methods.
Number 1 is a Turing reduction. In a Turing reduction from $A$ to $B$ you show an algorithm that can solve $A$ if it has access to an oracle for $B$ -- that is, at any time the algorithm for $A$ can decide to construct an instance of problem $B$ and instantaneously get a correct answer from the oracle. The algorithm is allowed to ask as many questions of the oracle as it wants to, and it can use the answers for anything, including to use them for deciding what its next question is going to be.
In your example the algorithm asks only one question. The example is not worded using the "oracle" terminology, but says "assume we have a machine that decides $B$" instead of "assume we have an oracle for $B$". For most purposes this makes no difference, but theoretical work often favors the "oracle" wording, such as to exclude arguments that go
(These arguments are valid, if a bit pointless, as far as proving undecidability of $B$ goes, but they are not really Turing reductions, and in some theoretical contexts we're interested in whether two problems that are both already known to be undecidable are Turing reducible to each other).
Number 2 is a many-one reduction. In a many-one reduction from $A$ to $B$ you show an algorithm for converting any instance of $A$ to an instance of $B$ that has the same answer as the input $A$ instance.
Of course, whenever you have a many-one reduction you can easily get a Turing reduction -- just replace "return X" in the many-one-reduction with "ask the oracle about X and return its answer".
However, a Turing reduction can't necessarily be rewritten as a many-one reduction. For example let DIVERGE${}_{\mathit{TM}}$ be the set of all Turing machines that don't halt. There are easy Turing reductions from HALT to DIVERGE and vice versa (just ask the oracle about your input and invert the answer), but there cannot be a many-one reduction from HALT to DIVERGE (or vice versa) because that would make HALT both r.e. and co-r.e., which would make it decidable.
Many-one reductions are thus a weaker technique than Turing machines for showing undecidability. But this also means that the existence of a many-one reduction gives more fine-grained information about the relation between problems. You can use many-one reductions to show that a problem is or isn't recursively enumerable (which Turing reductions show nothing about). And in complexity theory, NP-completeness and several other complexity classes are explicitly defined by many-one reductions.