At the risk of starting some kind of (un?)civil war, let me expand on my comments.
First and foremost, let's address the interpretation of the question. The OP asks "do we need a model category of spectra". If we interpret need to mean "without a model category of spectra we are unable to prove our favorite theorems and make our favorite computations" I think the answer is straightforward: no we do not need it. As I said in the comments:
- Computations are largely done in the homotopy category, unless they use the existence of certain spectral sequences and extra structure that might act on them. However, to the best of my knowledge, all such spectral sequences together with whatever extra structure you like, can be constructed in the land of $\infty$-categories without mentioning any of the fancy model categories of spectra.
- I know of no homotopically meaningful result about spectra that requires one of the model categories of spectra.
So it is cheating to say: "$\infty$-categories can't prove that such and such is a strict, point-set symmetric monoidal widget" because you can't even ask that question in the land of $\infty$-categories. The real question is: have we ever actually needed to know there is some strict, point-set model for these things? I have asked many people to give me an example. I have never heard of one. I am not arguing that model categories for every concept are never used. One usually needs, at some point, some model category presenting spaces and/or one presenting $\infty$-categories when setting up the foundations. I am just saying that, once those foundations have been built, we do not need to go and find model categories for everything else in the world.
Now, as often happens in these discussions, the conversation has turned to a different question entirely: Are there things that are easier to prove with model categories of spectra than with the $\infty$-category of spectra?
This is the sort of question addressed by Dmitri above.
For the most part, I think this is very subjective: we all have different backgrounds and tastes, and whatever is easiest for us personally is what we should use.
However, I want to point out a subtlety in the discussion of this question. Let me take as our example the same as Dmitri's: constructing the Eilenberg-MacLane spectrum associated to a dga. Here is what Dmitri says:
Yes, the Eilenberg–MacLane functor from the category of differential-graded rings to the category of symmetric ring spectra in simplicial sets is constructed immediately using the lax monoidal structure of the Dold–Kan functor, whereas the analogous construction in the quasicategorical world is far more involved.
But there is a fundamental mismatch between the two tasks. Implicit in the phrase "the Eilenberg-MacLane functor" is the idea that there is a somehow 'unique' one that satisfies some properties we want it to satisfy. (Otherwise both parties would have an easy time constructing a symmetric monoidal functor from dgas to spectra: just send everything to zero.)
So the model category theorist, in answering this question, gets to: (i) choose a model for what 'dgas' are, (ii) choose a model for what 'spectra' are, and (iii) choose a specific model for what they mean by 'Eilenberg-MacLane' spectra. Then they show their construction is some type of monoidal and hopefully that it produces familiar homotopy types when applied on familiar dgas. (By the way: if we're allowed to pick whatever model is convenient, why not just take $\mathrm{H}\mathbb{Z}$-modules and the right adjoint to smashing with $\mathrm{H}\mathbb{Z}$?)
But now, the burden is on the model category theorist to:
- Check that this particular construction can be appropriately derived.
- Check that this particular construction agrees with the other particular construction produced by some other model category theorist.
- Check that this particular construction has all of my favorite properties. And, if it doesn't, that it is equivalent through some zig-zag of Quillen equivalences to some other construction which does.
- In verifying (3), one must re-verify (1) and (2) for these new properties.
For and example of (4): the Dold-Kan functor is not lax symmetric monoidal, but we would still like to know that a cdga gets mapped to an $\mathbb{E}_{\infty}$-algebra. (And, more generally, that a chain complex with an $\mathbb{E}_{\infty}$-structure gets mapped to an $\mathbb{E}_{\infty}$-ring). It is not really clear how to immediately deduce that with the set-up you give... and, if you did write down some explicit $\mathbb{E}_{\infty}$-algebra structure, you would then need to verify that everyone else that writes down an $\mathbb{E}_{\infty}$-algebra structure on some EM-functor equivalent to yours actually produced an equivalent gadget... and so on and so forth forever.
This becomes a very large enterprise. People writing down $n$-different explicit constructions in $n$-different model categories, comparing them, then realizing there is more structure on those constructions, and comparing those, etc. etc.
In the land of $\infty$-categories, you have to work harder to setup the theory but you prove stronger theorems. The functor $D(\mathbb{Z})_{\ge 0} \to \mathsf{Sp}$ producing Eilenberg-MacLane objects can be produced directly from universal properties of the left and right hand side as symmetric monoidal $\infty$-categories. It is then automatically characterized up to a contractible space of choices by various conditions, which provides automatic natural zig-zags of weak equivalences between whatever constructions you make with model categories that satisfy some list of conditions. Moreover, it automatically produces souped-up functors from algebras over any operad in $D(\mathbb{Z})_{\ge 0}$ to algebras over that same operad in $\mathsf{Sp}$. Finally, no computational strength is lost: all of your favorite spectral sequences and filtrations etc. arise from the fact that this functor preserves (homotopy) colimits and is easy to compute on free things.
Let me point out, also, that even having a characterization of this functor via universal properties helps you to check stuff like (4) above. It turns out that the space of ways to promote the plain-old EM-functor to an ($\infty$-)symmetric monoidal functor is contractible. So if some model category theorist goes and promotes their EM-functor to a lax symmetric monoidal one in two different ways, then they automatically know they agree up to some natural zig-zag of weak equivalences.
All of the above was about a specific example, but it is part of a larger point.
- The $\infty$-categorical setup allows us to characterize highly structured objects/categories/functors via universal properties and produce them via general existence results. You usually can't even state those universal properties with model categories.
- Computations with objects/categories/functors immediately follow from the characterization because eventually whatever you're doing is probably a bar construction and then, voila, you have a spectral sequence.
- It is often possible to promote constructions like this to even more highly structures constructions with minimal extra work.
- Comparison with any other specific construction, be they model categorical or $\infty$-categorical, is immediate from the universal characterization. Moreover, just the existence of a universal characterization of promoted versions of a construction produces non-obvious comparison results for constructions with model categories.