The proofs-as-programs paradigm which establishes a correspondence between formal proofs and computer programs has made tremendous impact on the world of computing, enabling various high-value applications in different areas of computer science. However, while the world of computing has benefited greatly from formal foundations through the proofs-as-programs paradigm, the benefits of the flow in the converse direction have yet to be fully explored. Accordingly, we seek to explore the ways in which broader notions of computation can influence and contribute to formal foundations. In this first talk we demonstrate how Church-Turing computability can be extended by Brouwer's notion of non-lawlike computability in the form of free choice sequences. Thus, we present an extension of Nuprl's type theory that embeds the notion of choice sequences, which provides a foundation for a fully intuitionistic version of Nuprl.