Following a brief outline of the contrast between classical mathematics and constructive mathematics--mathematics with intuitionistic logic--I sketch Richman's proof of Gleason's Theorem. I then discuss the First Main Theorem of Pour-El and Richards. In particular, I focus on the wild claim that the First Main Theorem establishes the impossibility of a constructive theory of unbounded operators.
Constructive Aspects of Gleason's Theorem and Unbounded Operators