Is "compact implies sequentially compact" consistent with ZF? Over at the nForum, we've been discussing sequential compactness.  The discussion led me to realise that I naively assumed that nets were simply Big Sequences, and that I could make a reasonable guess at how nets would behave by thinking of them as such.
Not so.  The crucial point, that I hadn't realised, was that subnets are not sub-nets in the way that subsequences are sub-sequences.
Where this came to light was in a discussion of the relationship between compactness and sequential compactness.  Compactness can be expressed as:

Every net has a convergent subnet.

Sequential compactness as:

Every sequence has a convergent subsequence.

So, in my naivety, I assumed that compactness implied sequential compactness since I could take a sequence, think of it as a net, find a convergent subnet, and - ta-da - there's my convergent subsequence.  The error, as Mike Shulman pointed out, is that not every subnet of a sequence is a subsequence.
And, indeed, there is a space that is compact but not sequentially compact.  Writing $I = [0,1]$ then $I^I$ is compact but not sequentially compact.  In particular, it is possible to find a sequence that has no convergent subsequence (the argument is a variant of Cantor's diagonal theorem) but that has plenty of cluster points and thus plenty of convergent subnets.
But the compactness of $I^I$ seems to require a Big Axiom (not quite the axiom of choice, or so I'm led to believe since $I$ is Hausdorff, but almost).  I say "seems to" since I'm not an expert and there may be a way to prove that this specific space, $I^I$, is compact with only the basic axioms of ZF.
That's basically my question, except that I'm a topologist so I'm more interested in the implications for topological stuff than in the exact relationship between the Axiom of Choice and Tychanoff's theorem (and since I can just read the nLab page to learn that!).  So, without further ado, here's the question:

Is "Compactness => Sequential Compactness" consistent with ZF?

This could be answered by a topologist since all it would require to show that this isn't so would be an example of a space that was compact but not sequentially compact and such that proving that didn't require any Big Axioms.
References:

*

*nLab pages: sequential compactness (has more details on the above example), nets (contains the crucial definition of a subnet), Tychonoff's theorem (contains a discussion of the axiomatic strength of this theorem)

*nForum discussion: sequential compactness
 A: The sequential compactness of $[0,1]^{\omega_1}$ is undecidable in ZFC: as noted above $[0,1]^{[0,1]}$ is not, so under CH $[0,1]^{\omega_1}$is not sequentially compact; on the other hand $\mathrm{MA}+\neg\mathrm{CH}$ it is sequentially compact. Thus the question is still open.

$\mathrm{MA}$ implies that any product of fewer than continuum many sequentially compact spaces is sequentially compact.
In the case of $\aleph_1$ many and when $\mathrm{MA}+\neg\mathrm{CH}$ is assumd you follow the proof for products with countably many factors and produce, given a sequence $(x_n)$ in the product, infinite subsets $A_\alpha$ of $\mathbb{N}$ such that $(x_n)$ restricted to $A_\alpha$ converges on the first $\alpha$ coordinates and such that $A_\alpha\setminus A_\beta$ is finite whenever $\beta<\alpha$.   $\mathrm{MA}+\neg\mathrm{CH}$ now implies there is an infinite set $A$ such that $A\setminus A_\alpha$ is finite for all $\alpha$. Then $(x_n)$ restricted to $A$ converges in the full product.

A very nice introduction is still Mary Ellen Rudin's article in the Handbook of Mathematical Logic.
A: This Problem is already solved. See Horst Herrlich: "The Axiom of Choice" Springer
A: If you let $X=\prod_{\mathbb{R}}[0,1]$. By Tychonoff's Theorem this is compact. But one can construct a nice sequence by diagonalization such that it has no converging subsequence: let such a subsequence consist of a bunch of $0$'s and $1$'s and it does not converge in $[0,1]$. This is basically your example.
Now if we don't want AC then just let $X=\prod_{\omega_1}[0,1]$: no need for AC here, this is compact in ZF. Indeed $\omega_1$ is already well ordered. This space is not sequentially compact.
So compactness does not imply sequentially compactness in ZF.
Now what I wrote might be complete nonsense I am just a beginner at that stuff but eh! why not try to write an answer!
Edit: any stuff that is going to  look like the Stone-Čech or involve ultrafilters is going to need some choice, so maybe we need an example that is not related to the structure of the Stone-Čech
Edit #2: hold on, what if we take an arbitrary product of Tychonoff Planks. So basically it looks like that $X=\prod_{A}[0,\omega_1]\times[0,\omega$]. This is compact. Is this sequentially compact? This is does not look like first countable.
