Higher Topos Theory- what's the moral? I've often seen Lurie's Higher Topos Theory praised as the next "great" mathematical book. As someone who isn't particularly up-to-date on the state of modern homotopy theory, the book seems like a lot of abstract nonsense and the initial developments unmotivated. I'm interested in what the tools developed concretely allow us to do.
What does HTT let us do that we previously were unable to?
Please note that I'm looking for concrete examples or theorems that can be expressed in terms of math that one doesn't need higher topos theory to understand. I'd also be interested in ways that the book has changed pre-existing perspectives on homotopy theory.
 A: It seems there are really two questions here:

*

*Why higher category theory? What questions can you pose without the language of higher category theory which are best answered using higher category theory?


*Why does Lurie's work specifically set the standard for the foundations of higher category theory?
These are really distinct questions. I'll leave it to others to address (1), and focus on (2). For this, I will refer back to an old answer of mine for a summary of some of the contents of HTT and HA. There, I said:

In Higher Topos Theory, Lurie accomplishes many things. Let me highlight a few:

*

*A study of the Joyal model structure and comparison to the Bergner model structure.


*A study of cartesian fibrations and straightening / unstraightening, the $\infty$-categorical analog of the Grothendieck construction. This is often viewed as the technical heart of Lurie's theory, since cartesian fibrations are used systematically to avoid writing down all the higher coherence data involved in $qCat$-valued functors.


*A development of the fundamental notions of category theory -- (co)limits, Kan extensions, cofinality, etc, allowing one to "do category theory" in the $\infty$-categorical setting.


*A development of the theory of presentable $\infty$-categories. The point here is to get access to (the most important instances of) Freyd's adjoint functor theorem in the $\infty$-categorical setting, and in particular the theory of localizations.


*The theory of (Grothendieck) $\infty$-toposes.
In the context of foundations, maybe it's worth also mentioning some of the contents of Higher Algebra:

*

*The Barr-Beck monadicity theorem. I tend to think of this, along with the adjoint functor theorem as "the only real theorems" of basic ordinary category theory.


*A theory of operads, allowing one to "do algebra" $\infty$-categorically.


*The theory of stable $\infty$-categories, playing roughly the roles of abelian categories and triangulated categories in the $\infty$-categorical setting.

So the reason that HTT and HA set the standard for the foundations of category theory is pretty self-evident. Nowhere else can one find such a comprehensive treatment! The 2500 pages in these books are there for a reason. Some pieces of HTT/HA were previously available in various sources, but some were not, and moreover HTT/HA synthesize them in coherent account. So you don't have to spend as much time as you otherwise would have to patching together results proven in slightly different frameworks using model-comparison results.
This is particularly striking from a historical perspective: in the days when HTT first appeared (almost 10 years ago now -- to call it "the next great mathematical book" is already a little behind the times I think: it's a current great mathematical book!), all of this was a dream. Lurie made it a reality.
I'll add on a personal note that my own most common mode of doing higher category theory is to pretend that everything is an ordinary category and freely use all the tools available there, until I've worked out a complete argument. After that I go through the process of looking up $\infty$-categorical analogs of each of the 1-categorical tools I've used in my argument. This works better than one might expect, because it's reasonable today to trust that most of these tools will indeed be available in the literature. That's thanks in large part to Lurie's work. Before Lurie, you could do something like this, but only if you were content to end up with incomplete arguments contingent on the dream of higher category theory working out. Today, I'd argue that higher category theory, among various mathematical disciplines, actually has a relatively high standard of rigor. That's thanks in part to Lurie's work setting the standard.

Let me close by sharing a sort of testimonial from Clark Barwick (originally from the homotopy theory chat room here on MO, in the context of another MO question). Thanks to user1092847 for digging this up in the comments below!
Clark Barwick on Lurie's impact with HTT:

... I feel a need to defend Jacob Lurie's writing. Let me take a rather selfish perspective, because I grew up alongside higher categories in some sense. I read preprints and papers of Rezk, Hirschowitz-Simpson, Simpson, Tamsamani, Toen, Joyal, Jacob's HTT-prototype on the arXiv, and others as a grad student (2001-05).
All of these works had the same feature: they were all organised around a specific goal, leaving the more serious work of a complete theory for a later time. There were all sorts of homotopy coherence issues that were left hanging.
So I developed my own point of view about these things and started writing a manuscript, the first little bit of which was my thesis.
By the time I was halfway through my first postdoc, I'd written a pile of 'prenotes' that did enough foundational work to ensure, e.g., that there was no confusion over 'how unique' an adjoint between ∞-categories is, how to prove the existence of all colimits in an ∞-category from, say, geometric realisations and coproducts, a theory of what we now call ∞-operads, etc., etc.
It all involved layer upon layer of giant combinatorial gadgets, and they were often fragile enough that I wasn't sure I had them layered correctly.
At around that time I met Jacob at a conference, and he mentioned that he'd revised the text he put on the arXiv to add a little more detail. I said that I'd love to see it. He sent me a PDF of 600 pages or so of HTT.
To my surprise and horror, he'd done everything I'd done, but more of it and far far better. He'd understood issues like cofinality in a way I didn't have access to with the models I was using. In his text, the proofs worked because of some very compact, very robust models he chose early on, following Joyal.
Those models required him to do a lot of pretty tedious technical labour in the first few sections, but it ensured that if something existed up to homotopy, it 'really' existed. (This always came down to selecting a section of a trivial fibration.) This meant that it was genuinely easy to understand the arguments.
When you look at a proof in HTT or HA or SAG, it's all there. He doesn't tell you that you 'can' find the argument – he gives you the argument! That's the real advantage of Jacob's arguments (and Joyal's before him) – they're completely convincing. You can actually check (and in rare cases, yes, correct) his proofs, because every individual object is so concrete. (Cf. claims about $A_{\infty}$-categories like the Fukaya category.)
After a few sleepless nights, I just gave up on what I was trying to develop. I was not going to try to compete. On the other hand, I didn't feel comfortable enough in the Joyal/Lurie perspective to really use their model, so I tried to do things in a model-independent way, as Rune suggests.
But even simple things, like constructing a symmetric monoidal functor between two symmetric monoidal ∞-categories when there isn't one for formal reasons, is very difficult from that perspective: the only path I saw was to check an infinite hierarchy of coherences.
It took me a long time to realise that the fibrational perspective was exactly designed to make it easy (or at least convincing) to write these things down. Jacob is actually providing you with the tools to perform explicit, nontrivial, non-formal constructions with higher categories in a precise, legible, and convincing way. That's what results like HTT.3.2.2.13 are all about.
Jacob's done this continually: at every turn, he's done an incredible service to the community by carving out not just a narrow path to a desired application, but an expansive tunnel through which a lot of us can travel. He offers incredibly refined, interlinking technologies that are ideal for people like me, at least. I'm in a particularly good position to appreciate that kind of labour, because I attempted it and failed where he succeeded.
Does he solve every problem or define every conceivable object? No, of course not. (And if it's tough to read now, what would it be like if he did? (However, I will point out that he does deal with general pro-objects in SAG.E.2.)) Is it possible to sharpen his results or use little techniques to get improvements on his results? Sure. But overall, I think that the precision, clarity, and thoroughness of Jacob's writing is something to which homotopy theory should aspire.

A: I'm going to give a general answer first, and a specific answer below. It is my opinion that when Jacob Lurie wrote Higher Topos Theory, he was channeling Grothendieck. When Grothendieck revolutionized algebraic geometry, I'm sure that to a lot of folk it seemed "like a lot of abstract nonsense and the initial developments unmotivated" to use the OP's words. However, over time, it became clear that the abstract approach in fact led to powerful new results that could be stated in the original language, just like the OP wanted.
Hence, to answer "what's the moral" to all this abstraction, it is instructive to look at Grothendieck's thoughts on his own program. An excellent source for this is Colin McLarty's The Rising Sea. McLarty writes:

Grothendieck describes two styles in mathematics. If you think of a theorem to be proved as a nut to be opened, so as to reach “the nourishing flesh protected by the shell”, then the hammer and chisel principle is: “put the cutting edge of the chisel against the shell and strike hard. If needed, begin again at many different points until the shell cracks—and you are satisfied”. He [Grothendieck] says:


I can illustrate the second approach with the same image of a
nut to be opened. The first analogy that came to my mind is of
immersing the nut in some softening liquid, and why not simply
water? From time to time you rub so the liquid penetrates better,
and otherwise you let time pass. The shell becomes more flexible
through weeks and months—when the time is ripe, hand pressure
is enough, the shell opens like a perfectly ripened avocado!


A different image came to me a few weeks ago. The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration...the sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so
far off you hardly hear it...yet it finally surrounds the resistant substance

There are lots of quotes from Grothendieck in this direction. Essentially, his goal was to understand at a deep level, and then results fell out naturally. In fact, this is how he accomplished the remarkable feat, discussed here, of solving 14 open problems provided by Schwartz, as a PhD student. Grothendieck's abstract approach paid off in algebraic geometry, and Lurie's has paid off (and will keep paying off) in homotopy theory.
There are many specific examples. In recent years, homotopy theorists have made tremendous strides in algebraic K-theory computations that bedeviled mathematicians for decades before. For example, consider the paper On the K-theory of $\mathbb{Z}/p^n$ by Benjamin Antieau, Achim Krause, and Thomas Nikolaus. This paper computes, expicitly, the algebraic K-theory of $\mathbb{Z}/p^n$. I remind you that Dan Quillen won a Fields Medal for computing the algebraic K-theory of $\mathbb{Z}/p$ but did not know how to compute it for $\mathbb{Z}/p^n$. The statement has nothing to do with $\infty$-categories, but they were certainly an essential part of the program that led to the proof, since they took care of technical details that prevented earlier attempts from getting off the ground.
Another example is Descent and vanishing in chromatic algebraic K-theory via group actions, by Dustin Clausen, Akhil Mathew, Niko Naumann, and Justin Noel, which solves the $p$-group case of the Galois descent conjecture of Ausoni-Rognes. Again, a statement that didn't require $\infty$-categories, and a proof that needs them in a fundamental way.
Lastly, the paper The Chromatic Nullstellensatz by Robert Burklund, Tomer M. Schlank, and Allen Yuan, proves the Chromatic Redshift Conjecture, one of the big open problems of chromatic homotopy theory, a field that provided some of our best techniques to date for computing the stable homotopy groups of spheres. Again, $\infty$-categories are essential for the proof, whereas the statement could have been understood in the 1970s.
EDIT: Of course, there are many more specific examples. In some sense, Lurie's program began with the goal of proving the Cobordism Hypothesis, a statement about models topological quantum field theories, from 1995. Of course, you don't need $\infty$-categories for the statement. In the same 1995 paper, Baez and Dolan made the Stabilization Hypothesis, which has multiple proofs in the past decade. Gepner and Haugseng wrote one such proof, using the language of $\infty$-categories.
A: Here is a belated addendum to the other answers. In short, I think the comparison with Grothendieck is on point. More specifically I want to argue that HTT accomplished for higher category theory what EGA accomplished for scheme theory. (In particular I guess I am also arguing that the comments making comparisons between HTT and the Weil conjectures are somehow off base. I really mean EGA.)
In Récoltes et Semailles, Grothendieck describes the introduction of schemes as one the twelve "great ideas" of his mathematical life. And the definition of a scheme really is brilliant. At first sight it appears strange and unnecessarily abstract compared to the seeming simplicity of the definition of a classical algebraic variety. But as everyone knows now, schemes actually make your life simpler as an algebraic geometer. For years after first having gotten used to dealing with schemes I would have little lightbulb moments where I realized again something about why this exact definition is exactly the right one.
But Grothendieck did not just formulate the definition of a scheme. He also realized that for this to ever be used by anyone as a practical foundation of algebraic geometry, the entire edifice of algebraic geometry would need to be rebuilt from the ground up, including giving many nontrivial proofs of statements whose analogues in classical algebraic geometry were obvious. Thus the need for EGA. Of course there are new and important theorems in EGA as well, like the theorem on formal functions, but when people say that it is a monumental achievement they mean that it succeeded in usefully rebuilding algebraic geometry from scratch. In a hypothetical world where Grothendieck had advocated for the notion of a scheme but EGA had never been written, algebraic geometers would have continued to work exclusively with varieties through the years, even though some experts would have been aware that some better foundations should be possible.
This is more or less what happened in homotopy theory. Boardman-Vogt defined the notion of a weak Kan complex (quasicategory) as a model of homotopy theory already in 1973. We understand now that this is only one model for the theory of $\infty$-categories, but I think it is fair to say that compared to all other models it is striking in its radical simplicity (like the definition of a scheme). But after Boardman-Vogt very little happened for a long time. And without downplaying the work of Joyal and others I think is fair to say that Higher Topos Theory represented for the first time a reworking of the whole edifice of category theory and homotopy theory in the language of quasicategories, to the point where other people could meaningfully use it as a theory without working out an enormous amount of foundational material to even get off the ground. And like schemes, the role of quasicategories is to make your life simpler. Obviously homotopy theorists still use e.g. model categories (like algebraic geometers still use varieties) but I think it is fair to say that by now the introduction of $\infty$-categories has reshaped homotopy theory to the point where nobody in the field can just ignore them and keep working the same way as pre-Lurie. This is the accomplishment of HTT, rather than any one specific theorem from the book.
But I can see that this is a "hard sell" for outsiders, and I do think it is fair to say that higher category theory has not seen any application as remarkable as the proof of the Weil conjectures. (On the other hand it seems unfair to make a comparison with one of the greatest achievements of 20th century mathematics - it's not the standard we usually apply when judging new mathematics.) Although you'll find a preprint posted to the arXiv showing the use of higher category theory in practice pretty much every day, most of these applications are not applications in the sense that they could not have been written without the $\infty$-categorical formalism, but rather that they allow more conceptual proofs of stronger statements. As a particular example consider Fargues-Scholze's "Geometrization of the local Langlands correspondence". It is obviously spectacular work. It also uses $\infty$-categories in a serious way. But could it have been written without  $\infty$-categories? My guess: probably yes, at least most of it, but maybe not the parts on solid modules (and then with complications in dealing with adic coefficients). And only at the expense of more complications.
I hesitate a bit to add more to the existing comprehensive answers, but I hope this is of some value, too.
