Suppose I start a proof off with "Let $U_x$ be an open cover of $[0,1]$. Either $[0,1] \in U_x$ or $[0,1] \notin U_x$." Am I using the Law of the Excluded Middle here, or is this fact somehow evident without that assumption?
Also, does a constructive proof (interpreted loosely) of the compactness of $[0,1]$ exist? Is the standard proof constructive in any sense? Asked another way, is there an algorithm (again, interpreted loosely) that takes an open cover of $[0,1]$ and returns a finite open cover?