So far, it seems like every question we ask about Turing machines is undecidable. As it turns out, this is not just an educated hunch, but it turns out to be a notable theorem. First, we'll try to formalize the notion of a property.
A property $P$ of a Turing machine is a semantic property if it depends on the language recognized by $M$ and not the syntactic structure of $M$. In other words, if $L(M_1) = L(M_2)$, then $M_1$ and $M_2$ have the same semantic properties.
A property $P$ can be expressed as a language consisting of exactly the encodings $\langle M \rangle$, where $M$ has property $P$. A semantic property $P$ is said to be non-trivial if there exists a TM $M_1$ such that $\langle M_1 \rangle \in P$ and a TM $M_2$ such that $\langle M_2 \rangle \not\in P$.
Then we have the following theorem.
Theorem (Rice). All non-trivial semantic properties of Turing machines are undecidable.
In other words, for any given Turing machine $M$, we can't decide any properties about $L(M)$ except for properties that are true for either exactly all or exactly none of the languages recognized by Turing machines.
Proof. To show this, we assume that $P$ is a decidable language that satisfies some property and we let $R_P$ be a TM that decides $P$. We will reduce TM membership to property testing.
Let $T_\emptyset$ be a TM that always rejects, so $L(T_\emptyset) = \emptyset$. Without loss of generality, we assume that $\langle T_\emptyset \rangle \not\in P$, since otherwise, we can just use $\overline P$ instead. Since $P$ is non-trivial, there exists a TM $T$ with $\langle T \rangle \in P$.
We construct a Turing machine that decides $A_{TM}$ by being able to distinguish between $T_\emptyset$ and $T$.
$M_w$ simulates $T$ if $M$ accepts $w$. Then $L(M_w) = L(T)$ if $M$ accepts $w$ and $L(M_w) = \emptyset$ otherwise. Thus, $\langle M_w \rangle \in P$ iff $M$ accepts $w$. $$\tag*{$\Box$}$$
Now we'll formalize the notion of reducibility and reduction. This is an important notion in theoretical computer science and while we've been getting away with ignoring it for now, this concept will become much more important when it appears again in complexity theory.
A function $f: \Sigma^* \to \Sigma^*$ is a computable function if some Turing machine $M$, on every input $w$, halts with only $f(w)$ left on its tape.
What kinds of functions are compuatble? We have fairly obvious examples such as arithmetic operations. For our purposes, we are more interested in transforming various kinds of input strings into other input strings. For instance, we can take as input some description of a Turing machine $\langle M \rangle$ and transform it into some other machine $\langle M' \rangle$. This is something that we've been implicitly doing when we assume that various machines can be constructed.
A language $A$ is mapping reducible to a language $B$, denoted $A \leq_M B$, if there is a computable function $f:\Sigma^* \to \Sigma^*$, where for every $w$, $$ w \in A \iff f(w) \in B.$$ The function $f$ is called the reduction from $A$ to $B$. The reduction is a formal way of specifying a transformation of an input string for a particular problem to an input string for some other problem.
Theorem. If $A \leq_m B$ and $B$ is decidable, then $A$ is decidable.
Proof. Let $M$ be a TM that decides $B$ and let $f$ be a reduction from $A$ to $B$. Then we can construct a TM that decides $A$ as follows:
From this we can see that $w \in A$ obviously implies $f(w) \in B$. $$\tag*{$\Box$}$$
This result also gives us the following corollary which we have been implicitly making use of.
Corollary. If $A \leq_m B$ and $A$ is undecidable, then $B$ is undecidable.
And in fact, we can get the following results about recognizability using the same arguments.
Theorem. If $A \leq_m B$ and $B$ is Turing-recognizable, then $A$ is Turing-recognizable.
Corollary. If $A \leq_m B$ and $B$ is not Turing-recognizable, then $A$ is not Turing-recognizable.
Let's consider the proof that $HALT_{TM}$ is undecidable. To show an explicit mapping reduction, we need to show that there exists a computable function $f$ that transforms strings $\langle M,w \rangle$ into strings $\langle M',w' \rangle$ where $$ \langle M,w \rangle \in A_{TM} \iff \langle M',w' \rangle \in HALT_{TM}.$$ To do this, we simply show that there is a TM that computes an appropriate function $f$:
$$\tag*{$\Box$}$$
This mapping is quite simple: an appropriate mapping $f$ maps all strings $\langle M \rangle$ to a string $\langle M,N \rangle$ where $N$ is a machine that rejects all inputs. $$\tag*{$\Box$}$$