Reverse mathematics of (co)homology? Background
Exercise 2.1.16b in Hartshorne (homework!) asks you to prove that if $0 \rightarrow F \rightarrow G \rightarrow H \rightarrow 0$ is an exact sequence of sheaves, and F is flasque, then $0 \rightarrow F(U) \rightarrow G(U) \rightarrow H(U) \rightarrow 0$ is exact for any open set $U$.  My solution to this involved the axiom of choice in (what seems to be) an essential way.  
Essentially, you are asking to $G(U) \rightarrow H(U)$ to be surjective when you only know that $G \rightarrow H$ is locally surjective.  Ordinarily, you might not be able to glue the local preimages of sections in $H(U)$ together into a section of $G(U)$,  but since $F$ is flasque, you can extend the difference on overlaps to a global section. This observation deals with gluing finitely many local preimages together.  Zorn's lemma enters in to show that you can actually glue things together even if the open cover of $U$ is infinite.
Now, I have not really studied sheaf cohomology, but the idea I have is that it detects the failure of the global sections functor to be right exact.  So if you can't even show sheaf cohomology vanishes for flasque sheaves without the axiom of choice, it seems like a lot of the machinery of cohomology would go out the window.
Now, just on the set theoretic level, it seems like there is something interesting going on here.  Essentially the axiom of choice is a local-global statement (although I had never thought of it this way before this problem), namely that if $f:X \rightarrow Y$ is a surjection you can find a way to glue the preimages $f^{-1}(\{y\})$ of a surjection together to form a section of the map $f$.
This brings me to my 
Questions
Can the above mentioned exercise in Hartshorne be proven without the axiom of choice?
How much homological machinery depends on choice?
Have any reverse mathematicians taken a look at sheaf cohomology as a subject to be "deconstructed"?
Have any constructive set theorists thought about using cohomological technology to talk about the extent to which choice fails in their brand of intuitionistic set theory? (it seems like topos models of such set theories might make the connection to sheaves and their cohomology very strong!)
My google-fu is quite weak, but searches for "reverse mathematics cohomology" didn't seem to bring anything up.
 A: I don't have Hartshorne, so I can't address the specifics of this case. However, there is a very interesting paper by Andreas Blass Cohomology detects failures of the Axiom of Choice (TAMS 279, 1983, 257-269), which addresses questions of this type and should at least put you on the right track.
A: 
Have any reverse mathematicians taken a look at sheaf cohomology as a subject to be "deconstructed"?

Colin McLarty has made a study of what it takes to define derived functor cohomology (with sheaf cohomology as a special case given a topos of sheaves). He finds that finite-order arithmetic (the union of $Z_n$ for $n=1,2,\ldots$) suffices

The large structures of Grothendieck founded on finite order arithmetic 
  Colin McLarty
(Submitted on 9 Feb 2011 (v1), last revised 30 Apr 2014 (this version, v4))
Abstract: Such large-structure tools of cohomology as toposes and derived categories stay close to arithmetic in practice, yet existing foundations for them go beyond the strong set theory ZFC. We formalize the practical insight by founding the theorems of EGA and SGA, plus derived categories, at the level of finite order arithmetic. This is the weakest possible foundation for these tools since one elementary topos of sets with infinity is already this strong. 
http://arxiv.org/abs/1102.1773

For Zariski cohomology of Noetherian schemes, one can use second order arithmetic

Zariski cohomology in second order arithmetic
  Colin McLarty
(Submitted on 2 Jul 2012 (v1), last revised 25 Jul 2012 (this version, v2))
Abstract: The cohomology of coherent sheaves and sheaves of Abelian groups on Noetherian schemes are interpreted in second order arithmetic by means of a finiteness theorem. This finiteness theorem provably fails for the etale topology even on Noetherian schemes. 
http://arxiv.org/abs/1207.0276

A: On any affine scheme and thus on any scheme with a finite affine cover (which I think most people would find a reasonable class of schemes to restrict to), any open cover has a finite subcover.  This property is usually called quasi-compact rather than compact for technical reasons.
I don't have Hartshorne with me, so I can't recite chapter and verse, but I know this is discussed somewhere in Hartshorne;  it's also covered by this nLab entry, though I suspect that's more technical than you're looking for.
