The report contains some basic logical results and observations relevant to the use of intuitionistic logic as a programming language. In particular, a Kripke completeness proof is given for a formalization of intuitionistic logic incorporating quasi-free identity, and it is argued that full intuitionistic logic is too complicated to be useful, in spite of its superficial "constructive" aspects.