I have now twice taught Galois theory to advanced high school students at PROMYS. This is a six week course, meeting four times a week, for students who already are comfortable with proofs and, in particular, have seen basic number theory. The second time, I taught the course as an IBL course, and you can read my worksheets here. Here is what I have done, and some thoughts about ways to do less.
Showing that there is no universal quintic formula: Both times, I started with a weak version of unsolvability of the quintic. This would make a very natural stopping point for a less ambitious course.
Consider the general degree $n$ polynomial
$$x^n + c_{n-1} x^{n-1} + \cdots + c_1 x + c_0 = (x-r_1) (x-r_2) \cdots (x-r_n).$$
Point out that $c_1$, ..., $c_n$ are symmetric polynomials in the roots $r_1$, ..., $r_n$. Exhibit the quadratic, cubic and (optionally) quartic formulas and point out that they compute they express the roots $r_i$ in terms of the coefficients $c_i$ while staying entirely inside the polynomials. For example, the quadratic formula is $r_1 = \tfrac{-c_1 + \sqrt{c_1^2-4c_2}}{2}$, and $c_1^2-4c_2 = (r_1-r_2)^2$, so you can take the square root without leaving the world of polynomials. (By prepared for discussions about what you mean by square root, since teachers have taught them that square roots are always positive; what you mean is any expression whose square is $c_1^2 - 4 c_2$.)
Announce that your goal is to show, for $n \geq 5$, that there is no expression for $r_1$, ..., $r_n$ in terms of $c_1$, ..., $c_n$, using the operators $+$, $-$, $\times$, $\div$, $\sqrt[n]{\ }$ such that every $n$-th root stays inside the symmetric rational functions. It is worth taking some time to get some buy in that students understand the goal and realize it is nontrivial and a reasonable approximation to what we might informally state as "there is no quintic formula".
With this as the goal, define the symmetric group $S_n$ and note how it acts on formulas in $r_1$, ..., $r_n$. Define the sign homomorphism $S_n \to \pm 1$ by the action of $S_n$ on $\prod_{i<j} (r_i - r_j)$ and define the alternating permutations $A_n$ as the permutations with sign $1$. Show that, for $n=3$ or $4$, there are polynomials which define homomorphisms $A_n \to \mathbb{C}^{\ast}$. Prove that, for $n \geq 5$, there are no homomorphisms $A_n \to \mathbb{C}^{\ast}$.
Now, define $F$ to be the set of all rational functions invariant for $A_n$. Clearly, $F$ is closed under $+$, $-$, $\times$, $\div$. Now the key Lemma: If $f \in F$ is nonzero, and $f = g^n$ for some $g$ in $\mathbb{C}(r_1, \dots, r_n)$, then $\sigma : \tfrac{\sigma(g)}{g}$ would be a group homomorphism $A_n \to \mathbb{C}^{\ast}$. But we showed (for $n \geq 5$) that there are no such homomorphisms! So $g$ must also be in $F$. Thus, our operations can never get us outside $F$, and in particular (for $n \geq 5$) we cannot get to $r_1$, $r_2$, ..., $r_n$. $\square$
I really like this approach because it introduces so many key concepts -- symmetries, characters, a set closed under the field operations, defining a subfield by its symmetries -- without ever needing to define a field or a group as an abstract object. The first time, I did the above argument in a week of lectures and then went back to point out the key abstractions of "field", "group" and "character" hiding in the proof. The second time, I did it in 3 weeks of IBL and introduced the group theory language explicitly as I went, but held back the definition of a field until we had completed the proof. Worksheet 9 is the climax.
As a side note, I never needed to prove the fundamental theorem of symmetric functions, though I assigned it as homework, and it is well-motivated by these results. The proof only needs the easy containment $\mathbb{C}(c_1, \ldots, c_n) \subseteq \mathbb{C}(r_1, \ldots, r_n)^{S_n}$, not the equality.
Getting to abstract fields If you want to do anything harder than this, I think you need to define fields.
Here, the fact that my students have already seen basic number theory is a huge advantage: They already know that, for $p$ a prime, every nonzero element of $\mathbb{Z}/p \mathbb{Z}$ is a unit, so they find it very quick to believe and prove the same thing about $k[x]/p(x) k[x]$ for $p(x)$ an irreducible polynomial.
There is a conceptual obstacle, though, which is convincing my students that they really can treat $\mathbb{Q}[\sqrt[3]{2}]$ as the same thing as $\mathbb{Q}[x]/(x^3-2) \mathbb{Q}[x]$. It takes them a long time to believe that, for example, knowing that $x^2+x+1$ is a unit in the ring $\mathbb{Q}[x]/(x^3-2) \mathbb{Q}[x]$ really proves that $\tfrac{1}{\sqrt[3]{2}^2+\sqrt[3]{2}+1}$ is in $\mathbb{Q}[\sqrt[3]{2}]$. I think it is worth spending time to make them sit with this discomfort until they resolve it.
There is a reasonable half way goal to aim for here -- that $\sqrt[3]{2}$ can't be computed with $+$, $-$, $\times$, $\div$, $\sqrt{\ }$. That has the advantage of using field extensions, and the multiplicativity of degree, but not splitting fields or Galois groups. I talked about that more here.
To my surprise, in summer 2021, I never actually wound up needing to prove that the degree of a field extension was well defined! I talked about bases and spanning sets, and showed that $1$, $x$, ..., $x^{\deg(f)-1}$ was a basis for $k[x]/f(x) k[x]$, but I never proved that two bases of a field had the same cardinality or that degree was multiplicative! This was quite a relief; in summer 2018, I took a week away from the main material to do a crash course on linear algebra, and I lost a lot of momentum there.
If you are going for the full unsolvability of the quintic
You need to introduce splitting fields and their automorphisms. At first, I found students swallow these with no hesitation, but they don't really realize what they've said yes to. When you tell them that there is an automorphism of $\mathbb{Q}[\sqrt[3]{2}, \omega]$ which maps $\sqrt[3]{2}$ to $\omega \sqrt[3]{2}$, the students who don't just say yes to everything will start to feel very concerned. I think this is probably the point where it pays off to have really gotten them used to the notion that computations with polynomials really do prove things about concrete subfields of $\mathbb{C}$.
The key lemma, from this perspective, is that if $f(x)$ is an irreducible polynomial in $F[x]$, and $K$ is a normal extension of $F$ in which $f$ has a root, then $f$ splits in $K$ and $\text{Aut}(K/F)$ acts transitively on the roots of $f$ in $K$. From this, deduce:
Theorem Suppose that $f(x)$ is an irreducible polynomial of degree $n \geq 5$ over $F_0$, let $K$ be a field in which $f$ splits and suppose that $\text{Aut}(K/F_0)$ acts on the roots of $f$ by $S_n$. Then there is no tower of radical extensions $F_0 \subset F_1 \subset \cdots \subset F_r$ in which $f(x)$ has a root.
It's worth taking the time to convince students that this really is a rigorous and powerful formalization of "you can't solve the quintic with radicals".
The key proof is to embed everything into a single splitting field $L$; let $G = \text{Aut}(L/F_0)$. The details are on Worksheet 17, but the key point is that, on the one hand, we have a surjection $G \to S_n$ but, on the other hand, we have a sequence of subgroups $G \trianglerighteq G_0 \trianglerighteq G_1 \trianglerighteq \cdots \trianglerighteq G_r = \{ e \}$ with each $G_{i+1}$ the kernel of a character $G_i \to \mathbb{C}^{\ast}$, and this is impossible. (The warm-up version that I start the course with is easier because $G$ is $S_n$, so we are building the composition series in a concrete group we know, rather than a very abstract group where all we can say is that it surjects to $S_n$.)
There are a surprising number of things I didn't need to prove! I never introduced the notion of separability; the result is correct as stated for a normal inseparable extension. I also never proved the fundamental theorem of Galois theory! This proof starts with a chain of subfields and uses it to construct a chain of subgroups, but we never need the reverse construction! In particular, if there were two different subgroups that stabilized the same subfield, it would not effect the proof in any way.
I also never needed the abstract notion of a quotient group! I always had a concrete homomorphism $G \to H$, and talked about its image and kernel; I never needed to show that every normal subgroup was the kernel of a homomorphism. I put this on the homework, but it was never used in class.
Once you get here, a final issue is to construct an explicit example of a polynomial where the Galois group is $S_n$. The easy root is to take the polynomial $x^n + c_{n-1} x^{n-1} + \cdots + c_1 x + c_0$ with coefficients in $\mathbb{C}(c_1, \ldots, c_n)$, since it is easy to see that $\text{Aut}{\big(} \mathbb{C}(r_1, \ldots, r_n)/\mathbb{C}(c_1, \ldots, c_n){\big)}$ is $S_n$.
If you want to give an actual quintic with coefficients in $\mathbb{Q}$ whose Galois group is $S_5$, there are various hacks to do this. What I did was to tell my students that, in 10 years, this would no longer be an issue: We will just write down a random polynomial $x^5 + c_4 x^4 + \cdots + c_0$ with integer coefficients and roots $(r_1, \ldots, r_5)$, compute the degree $120$ polynomial $g(x):= \prod_{\sigma \in S_5} {\big( }x-r_{\sigma(1)} - 2 r_{\sigma(2)} - \cdots - 5 r_{\sigma(5)} {\big)}$, and check that the result is irreducible; this will prove that the polynomial has Galois group $S_5$. The need for a clever proof is simply because modern computers can't* compute and factor such large polynomials. I then did show them the clever proof that an irreducible quintic with two complex roots has Galois group $S_5$, which was the last result of the course.
* I might be wrong about this! I just attempted the case of a random integer monic quintic on my laptop. The first time, I didn't use enough working precision in computing the roots, and the degree $120$ polynomial didn't even even have real coefficients. But I went back and told Mathematica to use 100 digits for every floating point computation, and it got the polynomial in quite reasonable time, with every coefficient within $10^{-90}$ of an integer. This could make a genuine in class demo! Of course, I would need to know whether I am actually computing the degree $120$ polynomial correctly, but it seems unlikely that floating point errors would come out so near integers every time. I'm not sure whether I can trust Mathematica's integer polynomial factorization for such large polynomials, but I know that Mathematica's routines for characteristic $p$ factorization are very good, and factoring my polynomial modulo the first $10$ primes finds a a degree $100$ factor modulo $3$; this is already enough to prove irreducibility. The future is now!
