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 categor. 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.

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 subleties, 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.

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.

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 spend time 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.)

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.)