A lot of ordinary math? I think there's one if not two exaggerations in there.
> My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it.
One of the things Friedman likes to emphasize about the foundation of math is that there is very little you actually need to do with it. A good foundation is one that you don't even need to know is there. Most mathematicians don't work in any formalism, so a foundation doesn't need to be useful. It's not as if anyone actually needs to do all those tedious set encodings.
Except that many of those who call for new foundations are really interested in mechanical proof checkers, and those do have to be useful. In order to make these arguments less religious, I think it would be worthwhile to adopt Turing's mathematical philosophy, which called for adopting mathematical foundations on an ad-hoc basis (or even no foundation at all). In other words, choose whatever foundation (if any) for the task at hand. This would make it easier to argue that, say, type theory is a more convenient core for proof checkers.
> This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable.
That's not how I read him. He thinks that FOL and ZFC are good enough, and as foundations don't matter in practice (a good foundation is one you can ignore; I think that's a quote by him), it would take some achievement to justify seriously considering alternatives. He even says what it would take: easier teaching and/or easier proofs. So far no alternative foundation has been able to improve either one.