revisiting $THH(\mathbb{F}_p)$ Reading through Bhatt-Morrow-Scholze's "Topological Hochschild Homology and Integral p-adic Hodge Theory" I encountered the following statement.

We use only “formal” properties of THH throughout the paper, with the
  one exception of Bökstedt’s computation of $THH(\mathbb{F}_p)$ ...

As a reminder, Bökstedt (and Breen?) computed $\pi_{*}THH(\mathbb{F}_p)$ as $\mathbb{F_p}[\sigma]$, where $\sigma$ is a polynomial generator in degree 2. Whereas ordinary (derived) Hochschild homology of $\mathbb{F_p}$ is easily seen to be a divided power algebra generated in the same degree, $\mathbb{F}_p\langle x\rangle.$ Note that in the latter algebra, writing $x^p = p! \frac{x^p}{p!}$ gives $x^p = 0,$ quite a different flavor than the topological theory.
At some point I looked this up and the computation appeared to rest on some not particularly formal spectral sequence manipulations which I was unable to follow. Is this still the situation? Has anyone revisited these computations recently?
 A: Alright, here is the promised answer. First, the Hopkins-Mahowald theorem states that $\mathbb{F}_p$ is the free $\mathbb{E}_2$-ring with $p=0$, i.e. it is the homotopy pushout in $\mathbb{E}_2$-rings of $S^0 \leftarrow \mathrm{Free}_{\mathbb{E}_2}(x) \rightarrow S^0$ where we have $x \mapsto 0$ for the first arrow and $x \mapsto p$ for the second arrow. 
Equivalently (after $p$-localization), if we let $S^1 \to \mathrm{BGL}_1(S^0_{(p)})$ be adjoint to $1-p \in \pi_0(S^0)_{(p)}^{\times}$, extend to a double loop map $\Omega^2S^3 \to \mathrm{BGL}_1(S^0_{(p)})$ and take the Thom spectrum, we get $\mathrm{H}\mathbb{F}_p$. At the prime 2 there are many references, and the original proof was due to Mahowald- it appears, for example, in his papers "A new infinite family in $\pi_*S^0$" and in "Ring spectra which are Thom complexes". At odd primes this is due to Hopkins-Mahowald, but it's hard to trace down the "original" reference- it appears, for example, in Mahowald-Ravenel-Shick "The Thomified Eilenberg-Moore Spectral Sequence" as Lemma 3.3. In both cases the result is stated in the Thom spectrum language. And, again, let me reiterate: this is a non-formal result and essentially equivalent to Bokstedt's original computation. One always needs to know Steinberger's result (proved independently in Bokstedt's manuscript) that $Q_1\tau_i = \tau_{i+1}$ mod decomposables in $\mathcal{A}_*$, where $Q_1$ is the top $\mathbb{E}_2$-operation. (I suppose one could get away with slightly less: one needs to know that $\tau_0$ generates $\mathcal{A}_*$ with $\mathbb{E}_2$-Dyer-Lashof operations).
Anyway, given this result, let's see how to compute THH. In Blumberg-Cohen-Schlichtkrull (https://arxiv.org/pdf/0811.0553.pdf) they explain how to compute THH of any $\mathbb{E}_1$-Thom spectrum, with increasingly nice answers as we add multiplicative structure. For an $\mathbb{E}_2$-Thom spectrum (i.e. one arising from a double loop map) we have that $\mathrm{THH}(X^{\xi}) \simeq X^{\xi} \wedge BX^{\eta B\xi}$ where $\eta B\xi$ is the composite $BX \to B(BGL_1(S^0)) \stackrel{\eta}{\to} BGL_1(S^0)$. So, in our case we have that $THH(\mathbb{F}_p) \simeq \mathbb{F}_p \wedge (\Omega S^3)^{\eta B\xi}$. Thom spectra are colimits, and smash products commute with those, so we can compute this smash product as the Thom spectrum of $BX \to B(BGL_1(S^0)) \to BGL_1(S^0) \to BGL_1(\mathbb{F}_p)$. But $\eta \mapsto 0$ in $\pi_*\mathrm{H}\mathbb{F}_p$ so this is the trivial bundle, and we deduce the result we're after:
$\mathrm{THH}(\mathbb{F}_p) \simeq \mathbb{F}_p \wedge \Omega S^3_+ \simeq \mathbb{F}_p[x_2]$. 

It's worth giving the same argument again but in a more algebraic way, and, as a bonus, you can basically see why the Blumberg-Cohen-Schlichtkrull result holds. 
The point (which is very well explained in a more general setting in Theorem 5.7 of Klang's paper here: https://arxiv.org/pdf/1606.03805.pdf) is that $\mathbb{F}_p$, as a module over $\mathbb{F}_p \wedge \mathbb{F}_p^{op}$, is obtained by extending scalars from $S^0$ as an $S^0[\Omega S^3_+]$-module. 
Indeed, start with the pushout of $\mathbb{E}_2$-algebras $S^0 \leftarrow \mathrm{Free}_{\mathbb{E}_2}(x) \to S^0$ and smash with $\mathbb{F}_p$ to get a pushout of $\mathbb{E}_2$-$\mathbb{F}_p$-algebras. But now both maps in the pushout are the augmentation, and we see that the map $\mathbb{F}_p \wedge \mathbb{F}_p \simeq \mathbb{F}_p \wedge \mathbb{F}_p^{op} \to \mathbb{F}_p$ is equivalent to the map $\mathrm{Free}_{\mathbb{E}_2-\mathbb{F}_p}(\Sigma x) \to \mathbb{F}_p$ which is just the augmentation. This is tensored up from the map $\mathrm{Free}_{\mathbb{E}_2}(\Sigma x) \to S^0$, so we get that $\mathrm{THH}(\mathbb{F}_p) \simeq \mathbb{F}_p \otimes_{\mathbb{F}_p \wedge \mathbb{F}_p} \mathbb{F}_p \simeq S^0 \otimes_{\mathrm{Free}_{\mathbb{E}_2}(\Sigma x)} \mathbb{F}_p \simeq S^0 \otimes_{\mathrm{Free}_{\mathbb{E}_2}(\Sigma x)} S^0 \otimes_{S^0} \mathbb{F}_p$.
The left hand factor is given by $\mathrm{Free}_{\mathbb{E}_1}(\Sigma^2x)$, which you can see in various ways. For example, this bar construction is the suspension spectrum of the relative tensor product in spaces $* \otimes_{\Omega^2 S^3} *$, which is the classifying space construction and yields $B(\Omega^2S^3) \simeq \Omega S^3$.

A: This computation was given a totally different proof, not using any of the ideas being discussed above by Franjou, Lannes, Schwartz in Autour de la cohomologie de Mac Lane des corps finis. [On the Mac Lane cohomology of finite fields] Invent. Math. 115 (1994), no. 3, 513–538.  The relevant groups are Tor groups in an appropriate functor category, and [FLS] use some clever resolutions, a fun but easy to prove vanishing result, and ordinary homological diagram chasing/shifting to get their result.  
All of this is much easier than the arguments by Breen and Bockstedt (or processed using Hopkins--Mahowald).  And their ideas opened the floodgates to other similar calculations -- especially after the Annals paper of Friedlander and Suslin that introduced the category of strict polynomial functors.
