The question used the phrase "still needed." This is a very loaded term, and the answer that you give will depend very strongly on how you interpret it. 1. If, as Dylan does, we interpret this as asking **whether some theorems make it mathematically necessary** to use one of these strict models, I suspect that the answer is ultimately no. My reason is a little different from Dylan's. Lima's thesis first introduced categories of spectra in 1958 or 1959. Since then there have been many, many models introduced (even Vogt's lectures from 1969 on Boardman's category give a table comparing 8 different ones, including those developed by Spanier and Whitehead). However, the operating principle is now this: a "model for the category of spectra" is something that is equivalent to Boardman's category of spectra; the core applications are to determining information about maps in the stable homotopy category, or about function spaces between objects. One possible interpretation is this: theorems about stable homotopy theory have already been theorems about the $(\infty,1)$-category of spectra _by definition_ for several decades. 2. If we ask, instead, **whether some developments would not have happened** without these strict models, I suspect that the answer is yes. The most prominent example that I can think of is, in equivariant stable theory, the notion of a strictly commutative G-ring spectrum. These encode strictly more structure than the "homotopical" version of a commutative ring spectrum. Now, in the decade after Hill-Hopkins-Ravenel, we have explanations that go back and explain that this is because the G-equivariant category extends to some kind of G-symmetric monoidal category. However, this doesn't alter the fact that the structure was discovered because the _strict_ notion turned out to encode more information than the homotopical one. <p> If you allow me unstable comments: topological commutative monoids, topological abelian groups, the Dold-Thom theorem on infinite symmetric products, and the Dold-Kan correspondence on simplicial abelian groups are all theorems that are about a strictly more rigid structure than the notion of "commutative monoid" from Higher Algebra. These are all tremendously important structures. It's not clear to me that they would have developed if we would have started from ground zero with a coherent version of the category of spaces. However, we should not overlook the human question: **whether the subject is easier to teach, learn, and understand** using a concrete model. As of writing, I cannot see any way to answer this other than with a resounding yes. There is a good reason why definitions of spectra like those in Adams or Bousfield-Friedlander are still used by people entering the subject: even with care and attention to their subtleties, they can be learned and understood very quickly. With a strict symmetric monoidal model, you can define algebra and module objects with a couple of diagrams; someone who assumes they exist and have good properties can be working with them very quickly. Asserting that things are just as easy to do with new models of higher categories overlooks the *cost* involved in learning how to effectively work with them. (This isn't new. For example, developing fluency with homotopy limits and colimits _always_ took some effort, because they remove one of abstract algebra's most useful tools--dramatic and unapologetic overkill--now that "imposing a relation" has higher consequences.) I have seen groups of intelligent people fluent in this language stumped for some time trying to translate a basic fact of category theory into new terms. We cannot demand that those interested in stable theory must learn higher category theory. This is not yet material that can be easily black-boxed. (I say all of this as someone who, at least in recent years, has been converted.) Not least, part of the problem is that it is difficult to appreciate the development of higher category theory before you have some familiarity with the problems that it solves (e.g. up to and including the old "permuting two circles" problem in stable theory). There are not really a lot of references yet that tell the story of _why_ coherent category theory is a good idea in homotopy theory. This is just one of a series of expository problems that can be squarely laid at the feet of people in my generation and older, and it will hopefully get better as time goes on.